algEquivOfAlgEquiv — Mathlib

English

The absolute separable closure is defined as the separable closure of the base inside the algebraic closure.

Русский

Абсолютное разделимое замыкание определяется как разделимое замыкание базы внутри алгебраического замыкания.

LaTeX

$$SeparableClosure F (AlgebraicClosure F)$$

Lean4

/-- If `E` and `K` are isomorphic as `F`-algebras, then `separableClosure F E` and
`separableClosure F K` are also isomorphic as `F`-algebras. -/
def algEquivOfAlgEquiv (i : E ≃ₐ[F] K) : separableClosure F E ≃ₐ[F] separableClosure F K :=
  (intermediateFieldMap i _).trans (equivOfEq (map_eq_of_algEquiv i))

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