mathlib

0c8fffe9 - fix(algebra/group/prod): fixes for #5563 (#5577)

fix(algebra/group/prod): fixes for #5563 (#5577) * rename `prod.units` to `mul_equiv.prod_units`; * rewrite it with better definitional equalities; * now `@[to_additive]` works: fixes #5566; * make `M` and `N` implicit in `mul_equiv.prod_comm`