pow — Mathlib

English

A version of the power rule for padicValNat: v_p(a^n) = n · v_p(a) for a ≠ 0.

Русский

Версия правила степеней для padicValNat: v_p(a^n) = n · v_p(a) при a ≠ 0.

LaTeX

$$$ a \\neq 0 \\Rightarrow v_p(a^n) = n \\cdot v_p(a) $$$

Lean4

/-- A version of `padicValRat.pow` for `padicValNat`. -/
protected theorem pow (n : ℕ) (ha : a ≠ 0) : padicValNat p (a ^ n) = n * padicValNat p a := by
  simpa only [← @Nat.cast_inj ℤ, push_cast] using padicValRat.pow (Nat.cast_ne_zero.mpr ha)

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