valuation_pow — Mathlib

English

For any x and natural n, v_p(x^n) = n·v_p(x).

Русский

Для любого x и натурального n выполняется v_p(x^n) = n·v_p(x).

LaTeX

$$$v_p(x^n) = n\,v_p(x)\quad (n \in \mathbb{N})$$$

Lean4

@[simp]
theorem valuation_pow (x : ℚ_[p]) : ∀ n : ℕ, (x ^ n).valuation = n * x.valuation
  | 0 => by simp
  | n + 1 => by
    obtain rfl | hx := eq_or_ne x 0
    · simp
    · simp [pow_succ, hx, valuation_mul, valuation_pow, _root_.add_one_mul]

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