map_one

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.AddValuation.map_one

English

The additive p-adic valuation sends 1 to 0.

Русский

Падикова оценка единице 1 сопоставляет 0.

LaTeX

$$addValuationDef(1) = 0$$

Lean4

@[simp]
theorem map_one : addValuationDef (1 : ℚ_[p]) = 0 := by
  rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]

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

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

Разделы

Аффилиация

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