pow — Mathlib

English

If p is prime and a has finite p-multiplicity, then a^k has finite p-multiplicity for every natural k.

Русский

Если p — простое, и a имеет конечную p-кратность, то a^k имеет конечную p-кратность для всякого натурального k.

LaTeX

$$$ \forall {k : \mathbb{N}}, FiniteMultiplicity p (a^k)$$$

Lean4

theorem pow {p a : α} (hp : Prime p) (hfin : FiniteMultiplicity p a) {k : ℕ} : FiniteMultiplicity p (a ^ k) :=
  match k, hfin with
  | 0, _ => ⟨0, by simp [mt isUnit_iff_dvd_one.2 hp.2.1]⟩
  | k + 1, ha => by rw [_root_.pow_succ']; exact hp.finiteMultiplicity_mul ha (ha.pow hp)

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