instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors

English

The algebraMap between 𝓞_K and 𝓞_L is injective.

Русский

Карта алгебраMap между 𝓞_K и 𝓞_L инъективна.

LaTeX

$$$\\operatorname{ker}(\\mathrm{algebraMap}_{\\mathcal{O}_K \\to \\mathcal{O}_L}) = \\{0\\}$$$

Lean4

instance : IsLocalization (Algebra.algebraMapSubmonoid (𝓞 K) ℤ⁰) K :=
  IsIntegralClosure.isLocalization_of_isSeparable ℤ ℚ K (𝓞 K)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru