factorMultiset_pow — Mathlib

English

For a positive natural n and exponent m, factorMultiset(n^m) = m • factorMultiset(n).

Русский

Для положительного числа n и натурального m выполняется: factorMultiset(n^m) = m • factorMultiset(n).

LaTeX

$$$ \\operatorname{factorMultiset}(n^m) = m \\cdot \\operatorname{factorMultiset}(n) $$$

Lean4

theorem factorMultiset_pow (n : ℕ+) (m : ℕ) : factorMultiset (n ^ m) = m • factorMultiset n :=
  by
  let u := factorMultiset n
  have : n = u.prod := (prod_factorMultiset n).symm
  rw [this, ← PrimeMultiset.prod_smul]
  repeat' rw [PrimeMultiset.factorMultiset_prod]

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