valuation_one

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

Let p be a prime. The p-adic valuation on the field ℚ_p assigns value 0 to the unit 1.

Русский

Пусть p — простое. Падиковая оценка на ℚ_p отдает 0 единице 1.

LaTeX

$$$v_p(1) = 0$$$

Lean4

@[simp]
theorem valuation_one : valuation (1 : ℚ_[p]) = 0 := by
  rw [← Nat.cast_one, valuation_natCast, padicValNat.one, cast_zero]
    -- not @[simp], since simp can prove it

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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