pow — Mathlib

English

For any nonzero rational q and any natural k, the p-adic valuation of q^k is k times the valuation of q: v_p(q^k) = k · v_p(q).

Русский

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

LaTeX

$$$ q \\neq 0 \\Rightarrow v_p(q^k) = k \\cdot v_p(q) $$$

Lean4

/-- A rewrite lemma for `padicValRat p (q^k)` with condition `q ≠ 0`. -/
protected theorem pow {q : ℚ} (hq : q ≠ 0) {k : ℕ} : padicValRat p (q ^ k) = k * padicValRat p q := by
  induction k <;> simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ', add_mul, add_comm]

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