[Merged by Bors] - feat(GroupWithZero): monoid with zero homs to (co)products#25466

pechersky wants to merge 25 commits intomasterleanprover-community/mathlib4:masterfrom

pechersky/g-w-zero-prodleanprover-community/mathlib4:pechersky/g-w-zero-prodCopy head branch name to clipboard