a b : ℕ
hab : coprime a b
⊢ (factorization a + factorization b).support = (factorization a).support ∪ (factorization b).support
a b : ℕ
hab : coprime a b
⊢ (factorization (a * b)).support = (factorization a).support ∪ (factorization b).support
rw [factorization_mul_of_coprime hab]
no goals
a b : ℕ
hab : coprime a b
⊢ (factorization a + factorization b).support = (factorization a).support ∪ (factorization b).support
exact support_add_eq (factorization_disjoint_of_coprime hab)