extension_algebra_isIntegral — Mathlib

English

Any extension between rings of integers is integral: 𝓞_L is integral over 𝓞_K.

Русский

Любое расширение между кольцами целых интегрально: 𝓞_L над 𝓞_K.

LaTeX

$$$\\mathcal{O}_L \\text{ is integral over } \\mathcal{O}_K$$$

Lean4

/-- Any extension between ring of integers is integral. -/
instance extension_algebra_isIntegral : Algebra.IsIntegral (𝓞 K) (𝓞 L) :=
  IsIntegralClosure.isIntegral_algebra (𝓞 K) L

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