equiv — Mathlib

English

Let L and M be separable closures of K. Then there exists a K-algebra isomorphism between L and M.

Русский

Пусть L и M — сепарабельные замыкания K. Тогда существует изоморфизм по K между L и M.

LaTeX

$$$\\exists \\varphi:\\; L \\cong_K M$$$

Lean4

/-- A (random) isomorphism between two separable closures of `K`. -/
noncomputable def equiv : L ≃ₐ[K] M :=
  AlgEquiv.ofBijective _
    (Normal.toIsAlgebraic.algHom_bijective₂ (IsSepClosed.lift : L →ₐ[K] M) (IsSepClosed.lift : M →ₐ[K] L)).1

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