mathlib3

cbb8f019 - feat(algebra/group/basic): prove `a / 1 = a` and remove `sub_zero` (#7956)

feat(algebra/group/basic): prove `a / 1 = a` and remove `sub_zero` (#7956) Add a proof that, in a group, `a / 1 = a`. As a consequence, `sub_zero` is the `to_additive version of this lemma and I removed it. The name of the lemma is `div_one'`, since the unprimed version is taken by `group_with_zero`. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60div_one'.60