Theorem: factorization_pow' (MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean)

State before:
n k p : ℕ
⊢ (n ^ k).factorization p = k * n.factorization p
Tactic:
rw [Nat.factorization_pow]
State after:
n k p : ℕ
⊢ (k • n.factorization) p = k * n.factorization p

State before:
n k p : ℕ
⊢ (k • n.factorization) p = k * n.factorization p
Tactic:
rfl
State after:
no goals