pow_factors — Mathlib

English

For any nonzero a and any natural k, the factors of a^k equal k copies of the factors of a.

Русский

Для любого не нуля a и натурального k разложения a^k состоят из k копий разложения a.

LaTeX

$$$$\\forall a \\neq 0, \\forall k:\\; (a^k).factors = k \\cdot a.factors.$$$$

Lean4

@[simp]
theorem pow_factors [Nontrivial α] {a : Associates α} {k : ℕ} : (a ^ k).factors = k • a.factors := by
  induction k with
  | zero => rw [zero_nsmul, pow_zero]; exact factors_one
  | succ n h => rw [pow_succ, succ_nsmul, factors_mul, h]

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