mathlib

34ce7847 - refactor(algebra/group_with_zero/basic): Golf using division monoid lemmas (#14213)

refactor(algebra/group_with_zero/basic): Golf using division monoid lemmas (#14213) Make all eligible `group_with_zero` lemmas one-liners from `division_monoid` ones and group them within the file.