u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom (u + v)) = prod u * prod v
u v : PrimeMultiset
⊢ prod (u + v) = prod u * prod v
change (coePNatMonoidHom (u + v)).prod = _
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom u + ↑coePNatMonoidHom v) = prod u * prod v
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom (u + v)) = prod u * prod v
rw [coePNatMonoidHom.map_add]
no goals
u v : PrimeMultiset
⊢ Multiset.prod (↑coePNatMonoidHom u + ↑coePNatMonoidHom v) = prod u * prod v
exact Multiset.prod_add _ _