ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u<VAR>Field k<VAR>IsAlgClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>Field k<VAR>IsAlgClosed k<VAR>x : k<GOAL>∃ z, x = z * z
<VAR>k : Type u<VAR>Field k<VAR>IsAlgClosed k<VAR>p : k[X]<GOAL>p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)
<VAR>k : Type u<VAR>Field k<VAR>R : Type u_1<VAR>Ring R<VAR>IsAlgClosed k<VAR>f : R →+* k<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<GOAL>∃ x, Polynomial.eval₂ f x p = 0
<VAR>k : Type u<VAR>Field k<VAR>R : Type u_1<VAR>Field R<VAR>IsAlgClosed k<VAR>f : R →+* k<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<GOAL>∃ x, Polynomial.eval₂ f x p = 0
<VAR>k : Type u<VAR>Field k<VAR>R : Type u_1<VAR>CommRing R<VAR>IsAlgClosed k<VAR>Algebra R k<VAR>hinj : Function.Injective ⇑(algebraMap R k)<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<GOAL>∃ x, (Polynomial.aeval x) p = 0
<VAR>k : Type u<VAR>Field k<VAR>R : Type u_1<VAR>Field R<VAR>IsAlgClosed k<VAR>Algebra R k<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<GOAL>∃ x, (Polynomial.aeval x) p = 0
<VAR>k : Type u<VAR>Field k<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → ∃ x, Polynomial.eval x p = 0<GOAL>IsAlgClosed k
<VAR>k : Type u<VAR>Field k<VAR>k' : Type u<VAR>Field k'<VAR>e : k ≃+* k'<VAR>IsAlgClosed k<GOAL>IsAlgClosed k'
<VAR>k : Type u<VAR>Field k<VAR>IsAlgClosed k<VAR>p : k[X]<VAR>hp : Irreducible p<GOAL>p.degree = 1
<VAR>k : Type u_1<VAR>K : Type u_2<VAR>Field k<VAR>Ring K<VAR>IsDomain K<VAR>hk : IsAlgClosed k<VAR>Algebra k K<VAR>Algebra.IsIntegral k K<GOAL>Function.Surjective ⇑(algebraMap k K)
<VAR>k : Type u_1<VAR>K : Type u_2<VAR>Field k<VAR>CommRing K<VAR>IsDomain K<VAR>IsAlgClosed k<VAR>f : k →+* K<VAR>hf : f.IsIntegral<GOAL>Function.Surjective ⇑f
<VAR>k : Type u_1<VAR>K : Type u_2<VAR>Field k<VAR>Ring K<VAR>IsDomain K<VAR>IsAlgClosed k<VAR>Algebra k K<VAR>Algebra.IsAlgebraic k K<GOAL>Function.Surjective ⇑(algebraMap k K)
<VAR>k : Type u_1<VAR>K : Type u_2<VAR>Field k<VAR>Field K<VAR>IsAlgClosed k<VAR>Algebra k K<VAR>L : IntermediateField k K<VAR>Algebra.IsAlgebraic k ↥L<GOAL>L = ⊥
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsAlgClosed K<VAR>Algebra k K<VAR>p q : k[X]<GOAL>IsCoprime p q ↔ ∀ (a : K), (Polynomial.aeval a) p ≠ 0 ∨ (Polynomial.aeval a) q ≠ 0
<VAR>R : Type u<VAR>K : Type v<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>NoZeroSMulDivisors R K<VAR>self : IsAlgClosure R K<GOAL>Algebra.IsAlgebraic R K
<VAR>R : Type u<VAR>K : Type v<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>NoZeroSMulDivisors R K<VAR>self : IsAlgClosure R K<GOAL>IsAlgClosed K
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>Algebra k K<GOAL>IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K
<VAR>K : Type u<VAR>Field K<VAR>L : Type v<VAR>M : Type w<VAR>Field L<VAR>Algebra K L<VAR>Field M<VAR>Algebra K M<VAR>IsAlgClosed M<VAR>E : Type u_1<VAR>Field E<VAR>Algebra K E<VAR>Algebra L E<VAR>IsScalarTower K L E<VAR>Algebra.IsAlgebraic L E<GOAL>Function.Surjective fun φ => φ.comp (IsScalarTower.toAlgHom K L E)
<VAR>K : Type u_1<VAR>Field K<VAR>L : Type u_2<VAR>M : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>Field M<VAR>Algebra K M<VAR>IsAlgClosed M<VAR>Algebra.IsAlgebraic K L<GOAL>IsAlgClosed.lift_aux K L M = Classical.choice ⋯
<VAR>M : Type u_1<VAR>Field M<VAR>IsAlgClosed M<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Type u_3<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Algebra R M<VAR>NoZeroSMulDivisors R S<VAR>NoZeroSMulDivisors R M<VAR>Algebra.IsAlgebraic R S<GOAL>IsAlgClosed.lift = let_fun this := ⋯; let_fun this_1 := ⋯; let f := IsAlgClosed.lift_aux (FractionRing R) (FractionRing S) M; (AlgHom.restrictScalars R f).comp (AlgHom.restrictScalars R (Algebra.ofId S (FractionRing S)))
<VAR>K : Type u_1<VAR>J : Type u_2<VAR>L : Type v<VAR>Field K<VAR>Field J<VAR>Field L<VAR>Algebra K J<VAR>Algebra J L<VAR>IsAlgClosure J L<VAR>Algebra K L<VAR>IsScalarTower K J L<VAR>hKJ : Algebra.IsAlgebraic K J<GOAL>IsAlgClosure K L
<VAR>R : Type u<VAR>S : Type u_3<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>CommRing S<VAR>Field L<VAR>Field M<VAR>Algebra R M<VAR>NoZeroSMulDivisors R M<VAR>IsAlgClosure R M<VAR>Algebra S L<VAR>NoZeroSMulDivisors S L<VAR>IsAlgClosure S L<VAR>hSR : S ≃+* R<GOAL>(↑(IsAlgClosure.equivOfEquiv L M hSR)).comp (algebraMap S L) = (algebraMap R M).comp ↑hSR
<VAR>R : Type u<VAR>S : Type u_3<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>CommRing S<VAR>Field L<VAR>Field M<VAR>Algebra R M<VAR>NoZeroSMulDivisors R M<VAR>IsAlgClosure R M<VAR>Algebra S L<VAR>NoZeroSMulDivisors S L<VAR>IsAlgClosure S L<VAR>hSR : S ≃+* R<VAR>s : S<GOAL>(IsAlgClosure.equivOfEquiv L M hSR) ((algebraMap S L) s) = (algebraMap R M) (hSR s)
<VAR>R : Type u<VAR>S : Type u_3<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>CommRing S<VAR>Field L<VAR>Field M<VAR>Algebra R M<VAR>NoZeroSMulDivisors R M<VAR>IsAlgClosure R M<VAR>Algebra S L<VAR>NoZeroSMulDivisors S L<VAR>IsAlgClosure S L<VAR>hSR : S ≃+* R<VAR>r : R<GOAL>(IsAlgClosure.equivOfEquiv L M hSR).symm ((algebraMap R M) r) = (algebraMap S L) (hSR.symm r)
<VAR>R : Type u<VAR>S : Type u_3<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>CommRing S<VAR>Field L<VAR>Field M<VAR>Algebra R M<VAR>NoZeroSMulDivisors R M<VAR>IsAlgClosure R M<VAR>Algebra S L<VAR>NoZeroSMulDivisors S L<VAR>IsAlgClosure S L<VAR>hSR : S ≃+* R<GOAL>(↑(IsAlgClosure.equivOfEquiv L M hSR).symm).comp (algebraMap R M) = (algebraMap S L).comp ↑hSR.symm
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>Field F<VAR>Field K<VAR>Field A<VAR>Algebra F K<VAR>Algebra F A<VAR>Algebra.IsAlgebraic F K<VAR>IsAlgClosed A<VAR>x : K<GOAL>(Set.range fun ψ => ψ x) = (minpoly F x).rootSet A
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>Field F<VAR>Field K<VAR>Field A<VAR>Algebra F K<VAR>Algebra F A<VAR>Algebra.IsAlgebraic F K<VAR>L : IntermediateField F A<VAR>hL : ∀ (x : K), Polynomial.Splits (algebraMap F ↥L) (minpoly F x)<VAR>f : K →ₐ[F] A<GOAL>(IntermediateField.algHomEquivAlgHomOfSplits A L hL).symm f = f.codRestrict L.toSubalgebra ⋯
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>Field F<VAR>Field K<VAR>Field A<VAR>Algebra F K<VAR>Algebra F A<VAR>Algebra.IsAlgebraic F K<VAR>L : IntermediateField F A<VAR>hL : ∀ (x : K), Polynomial.Splits (algebraMap F ↥L) (minpoly F x)<VAR>φ₂ : K →ₐ[F] ↥L<GOAL>(IntermediateField.algHomEquivAlgHomOfSplits A L hL) φ₂ = L.val.comp φ₂
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>Field F<VAR>Field K<VAR>Field A<VAR>Algebra F K<VAR>Algebra F A<VAR>Algebra.IsAlgebraic F K<VAR>L : IntermediateField F A<VAR>hL : ∀ (x : K), Polynomial.Splits (algebraMap F ↥L) (minpoly F x)<VAR>f : K →ₐ[F] ↥L<VAR>x : K<GOAL>((IntermediateField.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap (↥L) A) (f x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>Field F<VAR>Field K<VAR>Field A<VAR>Algebra F K<VAR>Algebra F A<VAR>Algebra.IsAlgebraic F K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra F L<VAR>Algebra L A<VAR>IsScalarTower F L A<VAR>hL : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)<VAR>f : K →ₐ[F] L<VAR>x : K<GOAL>((Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap L A) (f x)
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<GOAL>Irreducible f.factor
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<GOAL>Fact (Irreducible f.factor)
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<VAR>hf1 : ¬IsUnit f<GOAL>f.factor ∣ f
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<VAR>hf : f.degree ≠ 0<GOAL>f.factor ∣ f
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<VAR>hf : f.natDegree ≠ 0<GOAL>f.factor ∣ f
<VAR>K : Type v<VAR>Field K<VAR>f g : K[X]<GOAL>IsCoprime f g ↔ ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A), (Polynomial.aeval a) f ≠ 0 ∨ (Polynomial.aeval a) g ≠ 0
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<VAR>hf : f.natDegree ≠ 0<GOAL>(Polynomial.X - Polynomial.C (AdjoinRoot.root f.factor)) * f.removeFactor = Polynomial.map (AdjoinRoot.of f.factor) f
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<GOAL>f.removeFactor.natDegree = f.natDegree - 1
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<VAR>n : ℕ<VAR>hfn : f.natDegree = n + 1<GOAL>f.removeFactor.natDegree = n
<VAR>K : Type v<VAR>Field K<VAR>n : ℕ<VAR>f : K[X]<GOAL>Polynomial.SplittingFieldAux (n + 1) f = Polynomial.SplittingFieldAux n f.removeFactor
<VAR>K : Type v<VAR>Field K<VAR>n : ℕ<VAR>f : K[X]<GOAL>algebraMap K (Polynomial.SplittingFieldAux (n + 1) f) = (algebraMap (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)
<VAR>n : ℕ<VAR>K : Type u<VAR>Field K<VAR>f : K[X]<VAR>_hfn : f.natDegree = n<GOAL>Polynomial.Splits (algebraMap K (Polynomial.SplittingFieldAux n f)) f
<VAR>n : ℕ<VAR>K : Type u<VAR>Field K<VAR>f : K[X]<VAR>_hfn : f.natDegree = n<GOAL>Algebra.adjoin K (f.rootSet (Polynomial.SplittingFieldAux n f)) = ⊤
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<GOAL>Polynomial.Splits (algebraMap K f.SplittingField) f
<VAR>K : Type v<VAR>Field K<VAR>f : K[X]<GOAL>Algebra.adjoin K (f.rootSet f.SplittingField) = ⊤
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>self : IsNormalClosure F K L<GOAL>⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>self : IsNormalClosure F K L<VAR>x : K<GOAL>Polynomial.Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<GOAL>normalClosure F K L = ⨆ f, f.fieldRange
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>h : IsNormalClosure F K L<GOAL>Normal F L
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>K' : IntermediateField F L<GOAL>normalClosure F K L ≤ K' ↔ ∀ (f : K →ₐ[F] L), f.fieldRange ≤ K'
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>f : K →ₐ[F] L<GOAL>f.fieldRange ≤ normalClosure F K L
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>Algebra.IsAlgebraic F K<GOAL>normalClosure F K L ≤ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)<GOAL>normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>Algebra.IsAlgebraic F K<GOAL>IsNormalClosure F K L ↔ (∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) ∧ normalClosure F K L = ⊤
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)<GOAL>IsNormalClosure F K ↥(normalClosure F K L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>ne : Nonempty (K →ₐ[F] L)<VAR>h : Normal F L<GOAL>normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>Algebra K L<VAR>IsScalarTower F K L<VAR>Normal F L<GOAL>normalClosure F K L = ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>Algebra K L<VAR>IsScalarTower F K L<GOAL>IntermediateField.restrictScalars F (IsScalarTower.toAlgHom K (↥(normalClosure F K L)) L).fieldRange = normalClosure F K L
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>K : IntermediateField F L<GOAL>K ≤ normalClosure F (↥K) L
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>K : IntermediateField F L<VAR>Normal F ↥K<GOAL>normalClosure F (↥K) L = K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>K : IntermediateField F L<VAR>Normal F L<GOAL>normalClosure F (↥K) L = ⨆ f, IntermediateField.map f K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>K : IntermediateField F L<VAR>Normal F L<GOAL>normalClosure F (↥K) L = ⨆ f, IntermediateField.map (↑f) K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>K K' : IntermediateField F L<VAR>Normal F L<VAR>h : K ≤ K'<GOAL>normalClosure F (↥K) L ≤ normalClosure F (↥K') L
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>x : IntermediateField F L<GOAL>(IntermediateField.closureOperator F L).IsClosed x = (normalClosure F (↥x) L = x)
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>(IntermediateField.closureOperator F L) K = normalClosure F (↥K) L
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ normalClosure F (↥K) L = K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ normalClosure F (↥K) L ≤ K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K ≤ K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : L ≃ₐ[F] L), IntermediateField.map (↑σ) K ≤ K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange = K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K = K
<VAR>F : Type u_1<VAR>L : Type u_3<VAR>Field F<VAR>Field L<VAR>Algebra F L<VAR>Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : L ≃ₐ[F] L), IntermediateField.map (↑σ) K = K
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : IntermediateField K L<GOAL>IntermediateField.map (AlgHom.id K L) E = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<GOAL>FiniteDimensional K ↥⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<GOAL>⊥.fixingSubgroup = ⊤
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<GOAL>⊤ ∈ fixedByFinite K L
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<GOAL>FiniteDimensional K ↥E1 → FiniteDimensional K ↥E2 → FiniteDimensional K ↥(E1 ⊔ E2)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : IntermediateField K L<VAR>σ : L ≃ₐ[K] L<GOAL>σ ∈ E.fixingSubgroup ↔ ∀ x ∈ E, σ x = x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>h12 : E1 ≤ E2<GOAL>E2.fixingSubgroup ≤ E1.fixingSubgroup
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>U : Set (L ≃ₐ[K] L)<GOAL>U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : IntermediateField K L<VAR>FiniteDimensional K ↥E<GOAL>IsOpen ↑E.fixingSubgroup
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : IntermediateField K L<VAR>FiniteDimensional K ↥E<GOAL>IsClosed ↑E.fixingSubgroup
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra.IsIntegral K L<GOAL>T2Space (L ≃ₐ[K] L)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra.IsIntegral K L<GOAL>IsTotallyDisconnected Set.univ
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<GOAL>⊤.fixingSubgroup = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>r : R<VAR>p : Polynomial R<VAR>hp : p ∈ nonZeroDivisors (Polynomial R)<GOAL>(Polynomial.taylor r) p ∈ nonZeroDivisors (Polynomial R)
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<VAR>p : Polynomial R<VAR>q : ↥(nonZeroDivisors (Polynomial R))<GOAL>(RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } = { toFractionRing := Localization.mk ((Polynomial.taylor r) p) ⟨(Polynomial.taylor r) ↑q, ⋯⟩ }
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<VAR>p q : Polynomial R<GOAL>(RatFunc.laurentAux r) ((algebraMap (Polynomial R) (RatFunc R)) p / (algebraMap (Polynomial R) (RatFunc R)) q) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p) / (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) q)
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<VAR>p : Polynomial R<GOAL>(RatFunc.laurentAux r) ((algebraMap (Polynomial R) (RatFunc R)) p) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<VAR>p q : Polynomial R<GOAL>(RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p / (algebraMap (Polynomial R) (RatFunc R)) q) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p) / (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) q)
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<VAR>p : Polynomial R<GOAL>(RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p) = (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<GOAL>(RatFunc.laurent r) RatFunc.X = RatFunc.X + RatFunc.C r
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r x : R<GOAL>(RatFunc.laurent r) (RatFunc.C x) = RatFunc.C x
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>f : RatFunc R<GOAL>(RatFunc.laurent 0) f = f
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>f : RatFunc R<GOAL>(RatFunc.laurent r) ((RatFunc.laurent s) f) = (RatFunc.laurent (r + s)) f
<VAR>R : Type u<VAR>CommRing R<VAR>hdomain : IsDomain R<VAR>r : R<GOAL>Function.Injective ⇑(RatFunc.laurent r)
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : Module.Dual R M<VAR>x : M<GOAL>((Module.dualPairing R M) v) x = v x
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : M<VAR>a : Module.Dual R M<GOAL>((Module.Dual.eval R M) v) a = a v
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type uM'<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>u : M →ₗ[R] M'<VAR>l : Module.Dual R M'<GOAL>(Module.Dual.transpose u) l = l ∘ₗ u
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type uM'<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>M'' : Type uM''<VAR>AddCommMonoid M''<VAR>Module R M''<VAR>u : M' →ₗ[R] M''<VAR>v : M →ₗ[R] M'<GOAL>Module.Dual.transpose (u ∘ₗ v) = Module.Dual.transpose v ∘ₗ Module.Dual.transpose u
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type uM'<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : (M →ₗ[R] R) × (M' →ₗ[R] R)<VAR>a : M × M'<GOAL>((Module.dualProdDualEquivDual R M M') f) a = f.1 a.1 + f.2 a.2
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type uM'<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M × M' →ₗ[R] R<GOAL>(Module.dualProdDualEquivDual R M M').symm f = (f ∘ₗ LinearMap.inl R M M', f ∘ₗ LinearMap.inr R M M')
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type uM'<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>φ : Module.Dual R M<VAR>ψ : Module.Dual R M'<GOAL>(Module.dualProdDualEquivDual R M M') (φ, ψ) = LinearMap.coprod φ ψ
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<GOAL>f.dualMap = LinearMap.lcomp R R f
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<GOAL>f.dualMap = Module.Dual.transpose f
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>g : Module.Dual R M₂<GOAL>f.dualMap g = g ∘ₗ f
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>g : Module.Dual R M₂<VAR>x : M₁<GOAL>(f.dualMap g) x = g (f x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>AddCommMonoid M₁<VAR>Module R M₁<GOAL>LinearMap.id.dualMap = LinearMap.id
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>M₃ : Type u_1<VAR>AddCommGroup M₃<VAR>Module R M₃<VAR>f : M₁ →ₗ[R] M₂<VAR>g : M₂ →ₗ[R] M₃<GOAL>f.dualMap ∘ₗ g.dualMap = (g ∘ₗ f).dualMap
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f.dualMap
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ ≃ₗ[R] M₂<VAR>g : Module.Dual R M₂<VAR>x : M₁<GOAL>(f.dualMap g) x = g (f x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>AddCommMonoid M₁<VAR>Module R M₁<GOAL>(LinearEquiv.refl R M₁).dualMap = LinearEquiv.refl R (Module.Dual R M₁)
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ ≃ₗ[R] M₂<GOAL>f.dualMap.symm = f.symm.dualMap
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>M₃ : Type u_1<VAR>AddCommGroup M₃<VAR>Module R M₃<VAR>f : M₁ ≃ₗ[R] M₂<VAR>g : M₂ ≃ₗ[R] M₃<GOAL>g.dualMap ≪≫ₗ f.dualMap = (f ≪≫ₗ g).dualMap
<VAR>R : Type u<VAR>CommSemiring R<VAR>f : Module.Dual R R<VAR>r : R<GOAL>f 1 * r = f r
<VAR>R : Type u<VAR>CommSemiring R<VAR>M₁ : Type v<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>f : Module.Dual R M₁<GOAL>LinearMap.range (LinearMap.dualMap f) = Submodule.span R {f}
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>i j : ι<GOAL>(b.toDual (b i)) (b j) = if i = j then 1 else 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<GOAL>(b.toDual ((Finsupp.total ι M R ⇑b) f)) (b i) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<GOAL>(b.toDual (b i)) ((Finsupp.total ι M R ⇑b) f) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>m : M<VAR>i : ι<GOAL>(b.toDual m) (b i) = (b.repr m) i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>i : ι<VAR>m : M<GOAL>(b.toDual (b i)) m = (b.repr m) i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>i : ι<GOAL>b.toDual (b i) = b.coord i