F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsAlgebraic F x
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
simp only [isAlgebraic_iff_isIntegral] at hS
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
this : Algebra.IsIntegral F { x // x ∈ Algebra.adjoin F S }
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
have : Algebra.IsIntegral F (Algebra.adjoin F S) := by
  rwa [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff]
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
this✝ : Algebra.IsIntegral F { x // x ∈ Algebra.adjoin F S }
this : IsField { x // x ∈ Algebra.adjoin F S }
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
this : Algebra.IsIntegral F { x // x ∈ Algebra.adjoin F S }
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
have := isField_of_isIntegral_of_isField' this (Field.toIsField F)
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
this✝ : Algebra.IsIntegral F { x // x ∈ Algebra.adjoin F S }
this : IsField { x // x ∈ Algebra.adjoin F S }
⊢ (adjoin F S).toSubalgebra = Algebra.adjoin F S
rw [← ((Algebra.adjoin F S).toIntermediateField' this).eq_adjoin_of_eq_algebra_adjoin F S] <;> rfl
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Set E
hS : ∀ (x : E), x ∈ S → IsIntegral F x
⊢ Algebra.IsIntegral F { x // x ∈ Algebra.adjoin F S }
rwa [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff]