case h
a b : ℕ
hab : coprime a b
q : ℕ
⊢ ↑(factorization (a * b)) q = ↑(factorization a + factorization b) q
a b : ℕ
hab : coprime a b
⊢ factorization (a * b) = factorization a + factorization b
ext q
no goals
case h
a b : ℕ
hab : coprime a b
q : ℕ
⊢ ↑(factorization (a * b)) q = ↑(factorization a + factorization b) q
rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]