F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ Subalgebra.map f (Algebra.adjoin F (rootSet p K)) = Subalgebra.map f ⊤ ↔ Algebra.adjoin F (rootSet p K) = ⊤
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ Algebra.adjoin F (rootSet p L) = AlgHom.range f ↔ Algebra.adjoin F (rootSet p K) = ⊤
rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]
no goals
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ Subalgebra.map f (Algebra.adjoin F (rootSet p K)) = Subalgebra.map f ⊤ ↔ Algebra.adjoin F (rootSet p K) = ⊤
exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff