instZero

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.instZero

English

The p-adic numbers contain a multiplicative identity.

Русский

В p-адических числах существует единица умножения.

LaTeX

$$1_{Padic_p} is the multiplicative identity$$

Lean4

instance : Zero ℚ_[p] := by infer_instance

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

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

Разделы

Аффилиация

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