instIsDomain

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The p-adic integers form a domain, i.e., there are no zero divisors in Z_p.

Русский

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

LaTeX

$$$$\text{IsDomain}(\mathbb{Z}_p).$$$$

Lean4

instance : IsDomain ℤ_[p] :=
  NoZeroDivisors.to_isDomain _

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

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

Разделы

Аффилиация

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