Theorem: factorization_pow' (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean)

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

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