valuation_p_lt_one

Mathlib.NumberTheory.Padics.ValuativeRel

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

← MathLib Explorer

English

For a prime p, the p-adic valuation v satisfies v(p) < 1.

Русский

Для простого p оценка v(p) меньше единицы.

LaTeX

$$$\\text{valuation}_p(p) < 1$$$

Lean4

@[simp]
theorem valuation_p_lt_one : v p < 1 := by
  simp [(isEquiv v (Padic.mulValuation)).lt_one_iff_lt_one, hp.out.ne_zero, inv_lt_one₀, ← log_lt_iff_lt_exp]

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

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

Разделы

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

Аффилиация

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