multiplicity_pow — Mathlib

English

Protected: If p is prime and a has FiniteMultiplicity p a, then (ha.pow p) provides FiniteMultiplicity for all powers a^k.

Русский

Защищено: если p — простое, и a имеет FiniteMultiplicity p a, то (ha.pow p) дает конечность кратности для всех степеней a^k.

LaTeX

$$$ (ha.pow p).multiplicity\_pow \Rightarrow \forall k, FiniteMultiplicity p (a^k) $$$

Lean4

protected theorem multiplicity_pow {p a : α} (hp : Prime p) (ha : FiniteMultiplicity p a) {k : ℕ} :
    multiplicity p (a ^ k) = k * multiplicity p a := by
  exact_mod_cast (ha.pow hp).emultiplicity_eq_multiplicity ▸ ha.emultiplicity_eq_multiplicity ▸ emultiplicity_pow hp

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