equivOfAlgebraic — Mathlib

English

Assuming that K is algebraic over J, there is a K-algebra isomorphism between L and M, where L and M are algebraic closures related to K and J.

Русский

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

LaTeX

$$$\\text{If } \\text{Algebra.IsAlgebraic } K J, \\; L \\text{ and } M \\text{ are algebraic closures, then } L \\cong_K M.$$$

Lean4

/-- A (random) isomorphism between an algebraic closure of `K` and an algebraic closure
  of an algebraic extension of `K` -/
noncomputable def equivOfAlgebraic [Algebra.IsAlgebraic K J] : L ≃ₐ[K] M :=
  have := Algebra.IsAlgebraic.trans K J L
  equivOfAlgebraic' K J _ _

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