Commit 2021-06-17 11:31 cbb8f019

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