map_eq_of_algEquiv — Mathlib

English

If E ≃ₐ[F] K, then the image of separableClosure F E under the algebra equivalence equals separableClosure F K.

Русский

Если существуют алгебраические эквиваленты E ≃ₐ[F] K, то образ separableClosure F E по эквивалентности равен separableClosure F K.

LaTeX

$$$(separableClosure F E).map i = separableClosure F K$ for i : E ≃ₐ[F] K$$

Lean4

/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `separableClosure F E`
under the map `i` is equal to `separableClosure F K`. -/
theorem map_eq_of_algEquiv (i : E ≃ₐ[F] K) : (separableClosure F E).map i = separableClosure F K :=
  (map_le_of_algHom i.toAlgHom).antisymm (fun x h ↦ ⟨_, (map_mem_separableClosure_iff i.symm).2 h, by simp⟩)

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