factorization_pow — Mathlib

English

For any n,k, the factorization of n^k equals k times the factorization of n.

Русский

Для любого n и k факторизация n^k равна k-кратной факторизации n.

LaTeX

$$$\\operatorname{factorization}(n^k) = k \\cdot \\operatorname{factorization}(n)$$$

Lean4

/-- For any `p`, the power of `p` in `n^k` is `k` times the power in `n` -/
@[simp]
theorem factorization_pow (n k : ℕ) : factorization (n ^ k) = k • n.factorization := by
  induction k with
  | zero => simp
  | succ k ih =>
    rcases eq_or_ne n 0 with (rfl | hn)
    · simp
    rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih, add_smul, one_smul, add_comm]

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