Commit 2024-04-23 06:58 03b47142

chore: Move WithZero material depending on GroupWithZero (#12351) Everything under Algebra.Group should be additivisable. Therefore I move the GroupWithZero instances for WithZero from Algebra.Group.WithOne.Defs and the whole of Algebra.Group.WithOne.Units to a new file Algebra.GroupWithZero.WithZero. I credit Mario for https://github.com/leanprover-community/mathlib/commit/ad92a9ba47f417916aab365d13db653fa8991a84 and Johan for https://github.com/leanprover-community/mathlib/pull/762. Use the opportunity to slightly clean up the code:

• Replace := by where in instance declarations
• Add missing explicit arguments to coe lemmas
• Add missing section ... end