F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (gen F α))
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F α
conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α]
no goals
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
α : E
⊢ IsIntegral F (gen F α) ↔ IsIntegral F (↑(algebraMap { x // x ∈ F⟮α⟯ } E) (gen F α))
rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective]