injective — Mathlib

English

There exists an 𝓞_K-algebra isomorphism between 𝓞_L and any integral closure R of 𝓞_K in L.

Русский

Существует изоморфизм 𝓞_L и любого интегрального замыкания 𝓞_K в L над 𝓞_K.

LaTeX

$$$\\mathcal{O}_L \\cong_{\\mathcal{O}_K} \\mathcal{R}$ for any IsIntegralClosure $\\mathcal{R}$ of $\\mathcal{O}_K$ in $L$$$

Lean4

/-- The algebraMap between ring of integers is injective. -/
theorem injective : Function.Injective (algebraMap (𝓞 K) (𝓞 L)) :=
  (RingHom.injective_iff_ker_eq_bot (algebraMap (𝓞 K) (𝓞 L))).mpr (ker_algebraMap_eq_bot K L)

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