coe_one

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

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

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem coe_one : (↑(1 : ℚ) : ℚ_[p]) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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