Commit 2024-03-07 05:27 c8969e40
View on Github →chore(Algebra/Group): Do not import GroupWithZero (#11202)
I am claiming that anything within the Algebra.Group folder should be additivisable, to the exception of MonoidHom.End maybe. This is not the case of NeZero, MonoidWithZero and MonoidWithZeroHom which were all imported to prove a few lemmas. Those lemmas are easily moved to another file.