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

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

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