zero_def

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

The zero of the p-adic numbers corresponds to the constant zero sequence.

Русский

Нуль p-адических чисел соответствует константной нулевой последовательности.

LaTeX

$$$0_{\\mathbb{Q}_p} = \\overline{0}$$$

Lean4

theorem zero_def : (0 : ℚ_[p]) = ⟦0⟧ :=
  rfl

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

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

Разделы

Аффилиация

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