map_le_of_algHom — Mathlib

English

The image of separableClosure F E under i is contained in separableClosure F K.

Русский

Образ separableClosure F E по i содержится в separableClosure F K.

LaTeX

$$$(separableClosure F E).map i \\le separableClosure F K$$

Lean4

/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `separableClosure F E`
under the map `i` is contained in `separableClosure F K`. -/
theorem map_le_of_algHom (i : E →ₐ[F] K) : (separableClosure F E).map i ≤ separableClosure F K :=
  map_le_iff_le_comap.2 (comap_eq_of_algHom i).ge

Похожие утверждения