algEquivOfAlgEquiv — Mathlib

English

If E and K are isomorphic as F-algebras, then algebraicClosure F E and algebraicClosure F K are isomorphic as F-algebras.

Русский

Если E и K изоморфны как F-алгебры, то их алгебраические замыкания над F также изоморфны над F.

LaTeX

$$$ (\\operatorname{algebraicClosure}_F(E)) \\cong_F (\\operatorname{algebraicClosure}_F(K)) $$$

Lean4

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

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