instIsLocalRing

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.instIsLocalRing

English

The p-adic integers Z_p form a local ring.

Русский

p-адические целые числа Z_p образуют локальный кольцо.

LaTeX

$$IsLocalRing(ℤ_[p]).$$

Lean4

instance : IsLocalRing ℤ_[p] :=
  IsLocalRing.of_nonunits_add <| by simp only [mem_nonunits]; exact fun x y => norm_lt_one_add

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

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

Разделы

Аффилиация

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