self_pow_inv

Mathlib.NumberTheory.Padics.PadicVal.Basic

URI: https://scilib.ai/kg/mathlib#padicValRat.self_pow_inv

← MathLib Explorer

English

For prime p and natural r, the p-adic valuation of (p^r)^{-1} equals -r.

Русский

Для простого p и натурального r, v_p((p^r)^{-1}) = −r.

LaTeX

$$$ v_p\\left(p^r\\right)^{-1} = -r $$$

Lean4

@[simp]
theorem self_pow_inv (r : ℕ) : padicValRat p ((p : ℚ) ^ r)⁻¹ = -r := by
  rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero), padicValRat.self hp.elim.one_lt,
    mul_one]

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

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

Разделы

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

Аффилиация

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