emultiplicity_pow_self — Mathlib

English

Let p be a prime element; then multiplicity p (p^n) = n for all n.

Русский

Пусть p — простое число; тогда кратность p (p^n) равна n для всех n.

LaTeX

$$$ multiplicity p (p^n) = n $$$

Lean4

theorem emultiplicity_pow_self {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) : emultiplicity p (p ^ n) = n :=
  by
  apply emultiplicity_eq_of_dvd_of_not_dvd
  · rfl
  · rw [pow_dvd_pow_iff h0 hu]
    apply Nat.not_succ_le_self

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