equiv — Mathlib

English

𝓞_K is equivalent to any integral closure of ℤ in K; i.e., there is a ring isomorphism between 𝓞_K and any such R.

Русский

𝓞_K эквивалентно любому интегральному замыканию ℤ в K; существует кольцо-изоморфизм.

LaTeX

$$$\\mathcal{O}_K \\cong \\mathcal{R}$ for any IsIntegralClosure $\\mathcal{R}$ of $\\mathbb{Z}$ in $K$.$$

Lean4

/-- The ring of integers of `K` are equivalent to any integral closure of `ℤ` in `K` -/
protected noncomputable def equiv (R : Type*) [CommRing R] [Algebra R K] [IsIntegralClosure R ℤ K] : 𝓞 K ≃+* R :=
  (IsIntegralClosure.equiv ℤ R K _).symm.toRingEquiv

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