ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>T : Set E<VAR>H : T ⊆ S<GOAL>T ⊆ ↑(IntermediateField.adjoin F S)
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>F⟮⟯ = ⊥
<VAR>F : Type u_3<VAR>E : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>IntermediateField.adjoin F Set.univ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>K : Subfield E<VAR>HF : Set.range ⇑(algebraMap F E) ⊆ ↑K<VAR>HS : S ⊆ ↑K<GOAL>(IntermediateField.adjoin F S).toSubfield ≤ K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>F' : Type u_3<VAR>Field F'<VAR>Algebra F' E<VAR>S S' : Set E<GOAL>↑(IntermediateField.adjoin F S) ⊆ ↑(IntermediateField.adjoin F' S') ↔ Set.range ⇑(algebraMap F E) ⊆ ↑(IntermediateField.adjoin F' S') ∧ S ⊆ ↑(IntermediateField.adjoin F' S')
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : Set E<GOAL>IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) = IntermediateField.adjoin F (S ∪ T)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>x : E<GOAL>IntermediateField.adjoin F (insert x ↑(IntermediateField.adjoin F S)) = IntermediateField.adjoin F (insert x S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : Set E<GOAL>IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F S)) T) = IntermediateField.restrictScalars F (IntermediateField.adjoin (↥(IntermediateField.adjoin F T)) S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>E' : Type u_3<VAR>Field E'<VAR>Algebra F E'<VAR>f : E →ₐ[F] E'<GOAL>IntermediateField.map f (IntermediateField.adjoin F S) = IntermediateField.adjoin F (⇑f '' S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<VAR>S : Set ↥K<GOAL>IntermediateField.lift (IntermediateField.adjoin F S) = IntermediateField.adjoin F (Subtype.val '' S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<VAR>α : ↥K<GOAL>IntermediateField.lift F⟮α⟯ = F⟮↑α⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<GOAL>IntermediateField.lift ⊥ = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<GOAL>IntermediateField.lift ⊤ = K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<GOAL>IntermediateField.adjoin F ↑K = K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<VAR>S : Set E<GOAL>IntermediateField.restrictScalars F (IntermediateField.adjoin (↥K) S) = IntermediateField.adjoin F (↑K ∪ S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<VAR>S : Set E<VAR>h : K ≤ IntermediateField.adjoin F S<GOAL>IntermediateField.extendScalars h = IntermediateField.adjoin (↥K) S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>L : Type u_3<VAR>L' : Type u_4<VAR>Field L<VAR>Field L'<VAR>Algebra F L<VAR>Algebra L E<VAR>Algebra F L'<VAR>Algebra L' E<VAR>IsScalarTower F L E<VAR>IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>IntermediateField.restrictScalars F (IntermediateField.adjoin L S) = IntermediateField.restrictScalars F (IntermediateField.adjoin L' S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>Algebra.adjoin F S ≤ (IntermediateField.adjoin F S).toSubalgebra
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S<GOAL>(IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>K : IntermediateField F E<VAR>h : K.toSubalgebra = Algebra.adjoin F S<GOAL>K = IntermediateField.adjoin F S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>hS : Algebra.adjoin F S = ⊤<GOAL>IntermediateField.adjoin F S = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>s : Set E<VAR>p : E → Prop<VAR>x : E<VAR>h : x ∈ IntermediateField.adjoin F s<VAR>mem : ∀ x ∈ s, p x<VAR>algebraMap : ∀ (x : F), p ((algebraMap F E) x)<VAR>add : ∀ (x y : E), p x → p y → p (x + y)<VAR>neg : ∀ (x : E), p x → p (-x)<VAR>inv : ∀ (x : E), p x → p x⁻¹<VAR>mul : ∀ (x y : E), p x → p y → p (x * y)<GOAL>p x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>α ∈ F⟮α⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>↑(IntermediateField.AdjoinSimple.gen F α) = α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>(algebraMap (↥F⟮α⟯) E) (IntermediateField.AdjoinSimple.gen F α) = α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>IsIntegral F (IntermediateField.AdjoinSimple.gen F α) ↔ IsIntegral F α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α β : E<GOAL>IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯ = F⟮α, β⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α β : E<GOAL>IntermediateField.restrictScalars F (↥F⟮α⟯)⟮β⟯ = IntermediateField.restrictScalars F (↥F⟮β⟯)⟮α⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>hS : ∀ x ∈ S, IsAlgebraic F x<GOAL>(IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>hα : IsIntegral F α<GOAL>F⟮α⟯.toSubalgebra = Algebra.adjoin F {α}
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>p : F[X]<GOAL>Polynomial.IsSplittingField F E p ↔ Polynomial.Splits (algebraMap F E) p ∧ IntermediateField.adjoin F (p.rootSet E) = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>p : F[X]<VAR>K : IntermediateField F E<GOAL>Polynomial.IsSplittingField F (↥K) p ↔ Polynomial.Splits (algebraMap F ↥K) p ∧ K = IntermediateField.adjoin F (p.rootSet E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>p : F[X]<VAR>hp : Polynomial.Splits (algebraMap F E) p<GOAL>Polynomial.IsSplittingField F (↥(IntermediateField.adjoin F (p.rootSet E))) p
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<GOAL>E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>Algebra.IsAlgebraic K ↥E2<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>Algebra.IsAlgebraic K ↥E1<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>FiniteDimensional K ↥E1<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>FiniteDimensional K ↥E2<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>Nonempty ι<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<GOAL>↑(iSup t) = ⋃ i, ↑(t i)
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>dir : Directed (fun x x_1 => x ≤ x_1) t<GOAL>(iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, FiniteDimensional K ↥(t i)<GOAL>FiniteDimensional K ↥(⨆ i ∈ s, t i)
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>ι : Type u_5<VAR>t : ι → IntermediateField K L<VAR>p : ι → K[X]<VAR>s : Finset ι<VAR>h0 : ∏ i ∈ s, p i ≠ 0<VAR>h : ∀ i ∈ s, Polynomial.IsSplittingField K (↥(t i)) (p i)<GOAL>Polynomial.IsSplittingField K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<GOAL>(IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E<GOAL>(IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F ↥L<GOAL>(IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<GOAL>Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E<GOAL>Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F ↥L<GOAL>Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>K : IntermediateField F E<GOAL>F⟮α⟯ ≤ K ↔ α ∈ K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>⨆ x ∈ S, F⟮x⟯ = IntermediateField.adjoin F S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>CompleteLattice.IsCompactElement F⟮x⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Finset E<GOAL>CompleteLattice.IsCompactElement (IntermediateField.adjoin F ↑S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>h : S.Finite<GOAL>CompleteLattice.IsCompactElement (IntermediateField.adjoin F S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, f i
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, IntermediateField.adjoin F ((minpoly F i.snd).rootSet E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ IntermediateField.adjoin F S<GOAL>∃ T, ↑T ⊆ S ∧ x ∈ IntermediateField.adjoin F ↑T
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>IntermediateField.adjoin F S = ⊥ ↔ S ⊆ ↑⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>F⟮α⟯ = ⊥ ↔ α ∈ ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>F⟮0⟯ = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>F⟮1⟯ = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>n : ℤ<GOAL>F⟮↑n⟯ = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>n : ℕ<GOAL>F⟮↑n⟯ = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<GOAL>Module.rank F ↥K = 1 ↔ K = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<GOAL>FiniteDimensional.finrank F ↥K = 1 ↔ K = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>Module.rank F ↥⊥ = 1
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>FiniteDimensional.finrank F ↥⊥ = 1
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>Module.rank (↥⊥) E = Module.rank F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>FiniteDimensional.finrank (↥⊥) E = FiniteDimensional.finrank F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>Module.rank (↥⊤) E = 1
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>FiniteDimensional.finrank (↥⊤) E = 1
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>Module.rank F ↥⊤ = Module.rank F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>FiniteDimensional.finrank F ↥⊤ = FiniteDimensional.finrank F E
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>Module.rank F ↥(IntermediateField.adjoin F S) = 1 ↔ S ⊆ ↑⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>Module.rank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>FiniteDimensional.finrank F ↥(IntermediateField.adjoin F S) = 1 ↔ S ⊆ ↑⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>FiniteDimensional.finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1<GOAL>⊥ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>h : ∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ = 1<GOAL>⊥ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1<GOAL>Subsingleton (IntermediateField F E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>h : ∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ = 1<GOAL>Subsingleton (IntermediateField F E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>h : ∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ ≤ 1<GOAL>⊥ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>h : ∀ (x : E), FiniteDimensional.finrank F ↥F⟮x⟯ ≤ 1<GOAL>Subsingleton (IntermediateField F E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>minpoly F (IntermediateField.AdjoinSimple.gen F α) = minpoly F α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>(Polynomial.aeval (IntermediateField.AdjoinSimple.gen F α)) (minpoly F α) = 0
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>h : IsIntegral F α<GOAL>(IntermediateField.adjoinRootEquivAdjoin F h) (AdjoinRoot.root (minpoly F α)) = IntermediateField.AdjoinSimple.gen F α
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<VAR>Fact (Irreducible p)<GOAL>K⟮AdjoinRoot.root p⟯ = ⊤
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>(IntermediateField.adjoin.powerBasis hx).gen = IntermediateField.AdjoinSimple.gen K x
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>(IntermediateField.adjoin.powerBasis hx).dim = (minpoly K x).natDegree
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>FiniteDimensional K ↥K⟮x⟯
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>Algebra.IsAlgebraic K ↥K⟮x⟯
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>FiniteDimensional.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>S : Set K<VAR>hprim : IntermediateField.adjoin F S = ⊤<GOAL>IntermediateField.adjoin E S = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>FiniteDimensional F E<VAR>hprim : F⟮α⟯ = ⊤<VAR>K : IntermediateField F E<GOAL>IntermediateField.adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<GOAL>∃ L, FiniteDimensional F ↥L ∧ n < FiniteDimensional.finrank F ↥L
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>FiniteDimensional K L<GOAL>(minpoly K x).natDegree ≤ FiniteDimensional.finrank K L
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>FiniteDimensional K L<GOAL>(minpoly K x).degree ≤ ↑(FiniteDimensional.finrank K L)
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>ι : Type u_4<VAR>t : ι → IntermediateField K L<VAR>h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)<GOAL>Algebra.IsAlgebraic K ↥(⨆ i, t i)
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>S : Set L<VAR>hS : ∀ x ∈ S, IsIntegral K x<GOAL>Algebra.IsAlgebraic K ↥(IntermediateField.adjoin K S)
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>S : Set L<VAR>Finite ↑S<VAR>hS : ∀ x ∈ S, IsIntegral K x<GOAL>FiniteDimensional K ↥(IntermediateField.adjoin K S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>K : Type u<VAR>Field K<VAR>Algebra F K<VAR>h : IsIntegral F α<VAR>x : { x // x ∈ (minpoly F α).aroots K }<GOAL>((IntermediateField.algHomAdjoinIntegralEquiv F h).symm x) (IntermediateField.AdjoinSimple.gen F α) = ↑x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>K : Type u<VAR>Field K<VAR>Algebra F K<VAR>h : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F K) (minpoly F α)<GOAL>Fintype.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree
<VAR>K : Type u<VAR>Field K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))<GOAL>Irreducible (f.comp g)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>t : Finset E<GOAL>(IntermediateField.adjoin F ↑t).FG
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : IntermediateField F E<GOAL>S.FG ↔ ∃ t, t.Finite ∧ IntermediateField.adjoin F t = S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>⊥.FG
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : IntermediateField F E<VAR>h : S.FG<GOAL>S.FG
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : IntermediateField F E<VAR>IsNoetherian F E<GOAL>S.FG
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Finset E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)<GOAL>P (IntermediateField.adjoin F ↑S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)<VAR>K : IntermediateField F E<VAR>hK : K.FG<GOAL>P K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)<VAR>K : IntermediateField F E<GOAL>P K
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hpq : q ∣ p<GOAL>(↑↑(AdjoinRoot.algHomOfDvd hpq).toRingHom).toFun = ⇑(AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯)
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hpq : q ∣ p<GOAL>(AdjoinRoot.algHomOfDvd hpq) (AdjoinRoot.root p) = AdjoinRoot.root q
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>h_eq : p = q<GOAL>(AdjoinRoot.algEquivOfEq hp h_eq).toFun = ⇑(AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯)
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>h_eq : p = q<GOAL>↑(AdjoinRoot.algEquivOfEq hp h_eq) = AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>h_eq : p = q<GOAL>(AdjoinRoot.algEquivOfEq hp h_eq) (AdjoinRoot.root p) = AdjoinRoot.root q
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>hpq : Associated p q<GOAL>(AdjoinRoot.algEquivOfAssociated hp hpq).toFun = ⇑(AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯)
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>hpq : Associated p q<GOAL>↑(AdjoinRoot.algEquivOfAssociated hp hpq) = AdjoinRoot.liftHom p (AdjoinRoot.root q) ⋯
<VAR>K : Type u_1<VAR>Field K<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>hpq : Associated p q<GOAL>(AdjoinRoot.algEquivOfAssociated hp hpq) (AdjoinRoot.root p) = AdjoinRoot.root q
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x y : L<VAR>hx : IsAlgebraic K x<VAR>h_ev : (Polynomial.aeval y) (minpoly K x) = 0<GOAL>minpoly K y = minpoly K x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x y : L<VAR>hx : IsAlgebraic K x<VAR>h_mp : minpoly K x = minpoly K y<GOAL>(minpoly.algEquiv hx h_mp) (IntermediateField.AdjoinSimple.gen K x) = IntermediateField.AdjoinSimple.gen K y
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>pb : PowerBasis K L<VAR>f : K[X]<GOAL>pb.equivAdjoinSimple ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f) = (Polynomial.aeval pb.gen) f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>pb : PowerBasis K L<GOAL>pb.equivAdjoinSimple (IntermediateField.AdjoinSimple.gen K pb.gen) = pb.gen
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>pb : PowerBasis K L<VAR>f : K[X]<GOAL>pb.equivAdjoinSimple.symm ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>pb : PowerBasis K L<GOAL>pb.equivAdjoinSimple.symm pb.gen = IntermediateField.AdjoinSimple.gen K pb.gen
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>S : IntermediateField K L'<GOAL>IntermediateField.map f (IntermediateField.comap f S) = S ⊓ f.fieldRange