valuation_natCast

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

For n ∈ ℕ, valuation(n in ℚ_p) equals padicValNat p n.

Русский

Для n ∈ ℕ, valuation(n в ℚ_p) равно padicValNat p n.

LaTeX

$$$\\mathrm{valuation}(n: \\mathbb{Q}_p) = \\mathrm{padicValNat}(p,n)$$$

Lean4

@[simp]
theorem valuation_natCast (n : ℕ) : valuation (n : ℚ_[p]) = padicValNat p n := by
  rw [← Rat.cast_natCast, valuation_ratCast, padicValRat.of_nat]

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

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

Разделы

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

Аффилиация

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