English
If i: E →ₐ[F] K is an F-algebra homomorphism, then i x belongs to algebraicClosure F K if and only if x belongs to algebraicClosure F E.
Русский
Если i: E →ₐ[F] K — гомоморфизм, сохраняющий F, то i x принадлежит algebraicClosure F K тогда и только тогда, когда x принадлежит algebraicClosure F E.
LaTeX
$$$$i x \in \text{algebraicClosure } F K \iff x \in \text{algebraicClosure } F E$$$$
Lean4
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
`algebraicClosure F K` if and only if `x` is contained in `algebraicClosure F E`. -/
theorem map_mem_algebraicClosure_iff (i : E →ₐ[F] K) {x : E} : i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E :=
by simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]
