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

State before:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ ↑(Nat.factorization (m * n)) p = ↑(Nat.factorization m) p + ↑(Nat.factorization n) p
Tactic:
rw [Nat.factorization_mul mnez nnez]
State after:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ ↑(Nat.factorization m + Nat.factorization n) p = ↑(Nat.factorization m) p + ↑(Nat.factorization n) p

State before:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ ↑(Nat.factorization m + Nat.factorization n) p = ↑(Nat.factorization m) p + ↑(Nat.factorization n) p
Tactic:
rfl
State after:
no goals