ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝¹⁵ : NormedAddCommGroup EB<VAR>inst✝¹⁴ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹³ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : ChartedSpace HB B<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝⁹ : NormedAddCommGroup EM<VAR>inst✝⁸ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝⁷ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁴ : (x : B) → AddCommMonoid (E x)<VAR>inst✝³ : (x : B) → Module 𝕜 (E x)<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : IsSmooth IB a<VAR>e✝ e'✝ : Pretrivialization F TotalSpace.proj<VAR>this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this✝ : FiberBundle F E := a.toFiberBundle<VAR>this : VectorBundle 𝕜 F E := toVectorBundle a<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<GOAL>∀ y ∈ e.baseSet ∩ e'.baseSet, ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') y) = smoothCoordChange IB a he he' y
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝¹⁵ : NormedAddCommGroup EB<VAR>inst✝¹⁴ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹³ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : ChartedSpace HB B<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝⁹ : NormedAddCommGroup EM<VAR>inst✝⁸ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝⁷ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁴ : (x : B) → AddCommMonoid (E x)<VAR>inst✝³ : (x : B) → Module 𝕜 (E x)<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : IsSmooth IB a<VAR>e✝ e'✝ : Pretrivialization F TotalSpace.proj<VAR>this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this✝ : FiberBundle F E := a.toFiberBundle<VAR>this : VectorBundle 𝕜 F E := toVectorBundle a<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) v = (smoothCoordChange IB a he he' b) v
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝¹⁵ : NormedAddCommGroup EB<VAR>inst✝¹⁴ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹³ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : ChartedSpace HB B<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝⁹ : NormedAddCommGroup EM<VAR>inst✝⁸ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝⁷ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁴ : (x : B) → AddCommMonoid (E x)<VAR>inst✝³ : (x : B) → Module 𝕜 (E x)<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : IsSmooth IB a<VAR>e✝ e'✝ : Pretrivialization F TotalSpace.proj<VAR>this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this✝ : FiberBundle F E := a.toFiberBundle<VAR>this : VectorBundle 𝕜 F E := toVectorBundle a<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>(↑(a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') { proj := b, snd := (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).symm b v }).2 = (↑e' { proj := b, snd := e.symm b v }).2
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝¹⁵ : NormedAddCommGroup EB<VAR>inst✝¹⁴ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹³ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : ChartedSpace HB B<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝⁹ : NormedAddCommGroup EM<VAR>inst✝⁸ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝⁷ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁴ : (x : B) → AddCommMonoid (E x)<VAR>inst✝³ : (x : B) → Module 𝕜 (E x)<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : IsSmooth IB a<VAR>e✝ e'✝ : Pretrivialization F TotalSpace.proj<VAR>this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this✝ : FiberBundle F E := a.toFiberBundle<VAR>this : VectorBundle 𝕜 F E := toVectorBundle a<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>b ∈ (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).baseSet ∩ (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he').baseSet
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : Nontrivial M<GOAL>nilpotencyLength R L M = 1 ↔ IsTrivial L M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : Nontrivial M<GOAL>IsTrivial L M ∧ lowerCentralSeries R L M 0 ≠ ⊥ ↔ IsTrivial L M
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>(𝓝 1).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ x✝¹ : ℝ<VAR>x✝ : E<GOAL>x✝ = x✝ / 1
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>i : M<VAR>hi : i ∈ ↑p<VAR>j : N<VAR>hj : j ∈ ↑q<GOAL>(fun m n => (f m) n) i j ∈ ↑(map₂ f p q)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>inst✝ : NoncompactSpace X<GOAL>DenseRange some
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>inst✝ : NoncompactSpace X<GOAL>Dense {∞}ᶜ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>x : R<GOAL>x ∈ finsetApprox bS adm ↔ ∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>x : R<GOAL>(x ≠ 0 ∧ ∃ a ∈ Finset.univ, (distinctElems bS adm) a.1 - (distinctElems bS adm) a.2 = x) ↔ ∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → AddSubgroup N<VAR>h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)<GOAL>Independent p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → AddSubgroup N<VAR>h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)<GOAL>Independent (⇑AddSubgroup.toIntSubmodule ∘ p)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>hst : ↑s ≃ ↑t<GOAL>s.Finite ↔ t.Finite
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>this : HasSum (fun n => 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x)) ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))<VAR>ofReal_two : ↑2 = 2<GOAL>HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x)) ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>this : HasSum (fun n => 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x)) ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))<VAR>ofReal_two : ↑2 = 2<VAR>n : ℕ<GOAL>1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x) = (1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2).re
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>this : HasSum (fun n => 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x)) ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))<VAR>ofReal_two : ↑2 = 2<GOAL>(-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))) = ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2).re
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = g_poly.natDegree<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = g_poly.natDegree<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>g_poly.rootSet (GaloisField p n) = Set.univ
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>∀ (x : GaloisField p n), x ∈ g_poly.rootSet (GaloisField p n)
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>∀ x ∈ ⊤, x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>∀ x ∈ Algebra.adjoin (ZMod p) ((X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField), x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>n✝¹ p : ℕ<VAR>h_prime : Fact (Nat.Prime p)<VAR>n✝ n : ℕ<VAR>h : n ≠ 0<VAR>g_poly : (ZMod p)[X] := X ^ p ^ n - X<VAR>hp : 1 < p<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n<VAR>nat_degree_eq : g_poly.natDegree = p ^ n<GOAL>∀ x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod p) (GaloisField p n)) ∪ (X ^ p ^ n - X).rootSet (X ^ p ^ n - X).SplittingField), x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>∀ x ∈ Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField, (aeval x) g_poly = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>(aeval 0) g_poly = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>(aeval 1) g_poly = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>∀ (x y : GaloisField (n✝ + 1) n), (aeval x) g_poly = 0 → (aeval y) g_poly = 0 → (aeval (x + y)) g_poly = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>∀ (x : GaloisField (n✝ + 1) n), (aeval x) g_poly = 0 → (aeval (-x)) g_poly = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n✝² n✝¹ n : ℕ<VAR>h : n ≠ 0<VAR>n✝ : ℕ<VAR>h_prime : Fact (Nat.Prime (n✝ + 1))<VAR>g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X<VAR>hp : 1 < n✝ + 1<VAR>aux : g_poly ≠ 0<VAR>key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n<VAR>nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n<VAR>x : GaloisField (n✝ + 1) n<VAR>hx : x ∈ Subring.closure (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪ (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)<GOAL>∀ (x y : GaloisField (n✝ + 1) n), (aeval x) g_poly = 0 → (aeval y) g_poly = 0 → (aeval (x * y)) g_poly = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>m : M<GOAL>((foldl Q f hf) n) ((ι Q) m) = (f m) n
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : Differentiable 𝕜 f<GOAL>(Differentiable 𝕜 fun y => f y + g y) ↔ Differentiable 𝕜 g
<VAR>θ : Angle<GOAL>(θ + ↑π).sin = -θ.sin
<VAR>x✝ : ℝ<GOAL>(↑x✝ + ↑π).sin = -(↑x✝).sin
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c d : α<VAR>hcb : c ≤ b<VAR>had : a ≤ d<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>(split I i x).iUnion = ↑I
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s t : Set β<GOAL>∀ (x : α), x ∈ r.core (s ∩ t) ↔ x ∈ r.core s ∩ r.core t
<VAR>s : ℝ<GOAL>Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
<VAR>s : ℝ<GOAL>Tendsto (Complex.ofReal' ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma ↑s))
<VAR>s : ℝ<GOAL>Complex.ofReal' ∘ s.GammaSeq = (↑s).GammaSeq
<VAR>s : ℝ<VAR>n : ℕ<GOAL>(Complex.ofReal' ∘ s.GammaSeq) n = (↑s).GammaSeq n
<VAR>s : ℝ<VAR>n : ℕ<GOAL>↑(↑n ^ s * ↑n ! / ∏ j ∈ Finset.range (n + 1), (s + ↑j)) = ↑n ^ ↑s * ↑n ! / ∏ j ∈ Finset.range (n + 1), (↑s + ↑j)
<VAR>s : ℝ<VAR>n : ℕ<GOAL>↑(↑n ^ s) * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x) = ↑n ^ ↑s * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x)
<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁷ : Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A A' B B' : C<VAR>inst✝⁶ : HasBinaryProduct A B<VAR>inst✝⁵ : HasBinaryProduct A' B'<VAR>inst✝⁴ : HasBinaryProduct (F.obj A) (F.obj B)<VAR>inst✝³ : HasBinaryProduct (F.obj A') (F.obj B')<VAR>inst✝² : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))<VAR>inst✝¹ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)<VAR>inst✝ : IsIso (prodComparison F A B)<GOAL>inv (prodComparison F A B) ≫ F.map prod.snd = prod.snd