feat(algebra/group/prod) Units of a product monoid (#5563)
feat(algebra/group/prod) Units of a product monoid (#5563)

Just a simple seemingly missing def





leanprover-community/mathlib,leanprover-community/mathlib