emultiplicity_pow — Mathlib

English

For α with Prime p, emultiplicity p (a^k) equals k times emultiplicity p a.

Русский

В кольце с простым p кратность emultiplicity p (a^k) равна k на кратность emultiplicity p a.

LaTeX

$$$ emultiplicity p (a^k) = k \cdot emultiplicity p a $$$

Lean4

theorem emultiplicity_pow {p a : α} (hp : Prime p) {k : ℕ} : emultiplicity p (a ^ k) = k * emultiplicity p a := by
  induction k with
  | zero => simp [emultiplicity_of_one_right hp.not_unit]
  | succ k hk => simp [pow_succ, emultiplicity_mul hp, hk, add_mul]

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