instCommRing

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The p-adic integers form a commutative ring under the inherited operations from the ambient p-adic field.

Русский

П-адические целые образуют коммутативное кольцо, унаследованное от окружающего поля p-адических чисел.

LaTeX

$$$\mathbb{Z}_p \text{ is a commutative ring}$$$

Lean4

instance instCommRing : CommRing ℤ_[p] :=
  inferInstanceAs <| CommRing (subring p)

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

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

Разделы

Аффилиация

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