no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
⊢ FactorSet.prod (⊤ + b) = FactorSet.prod ⊤ * FactorSet.prod b
simp
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : FactorSet α
⊢ FactorSet.prod (a + ⊤) = FactorSet.prod a * FactorSet.prod ⊤
simp
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ FactorSet.prod (↑a + ↑b) = FactorSet.prod ↑a * FactorSet.prod ↑b
rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]