[Merged by Bors] - refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids

[YaelDillies]

Delete the group and group_with_zero lemmas which have been made one-liners in #14000.

Lemmas are renamed because

• one of the group or group_with_zero name has to go
• the new API should have a consistent naming convention

Lemma renames

group lemma, group_with_zero lemma → new division_monoid/division_comm_monoid lemma

• -, inv_eq_of_mul_left_eq_one → inv_eq_of_mul_eq_one_left
• inv_eq_of_mul_eq_one, inv_eq_of_mul_right_eq_one → inv_eq_of_mul_eq_one_right
• eq_inv_of_mul_eq_one, eq_inv_of_mul_left_eq_one → eq_inv_of_mul_eq_one_left
• -, eq_inv_of_mul_right_eq_one → eq_inv_of_mul_eq_one_right
• -, eq_one_div_of_mul_eq_one → eq_one_div_of_mul_eq_one_right
• inv_div', inv_div → inv_div
• div_one', div_one → div_one
• eq_of_div_eq_one', eq_of_div_eq_one → eq_of_div_eq_one
• div_eq_inv_mul', div_eq_inv_mul → div_eq_inv_mul
• div_right_comm', div_right_comm → div_right_comm
• div_mul_eq_mul_div', div_mul_eq_mul_div → div_mul_eq_mul_div
• div_mul_comm, div_mul_comm' → div_mul_comm
• mul_comm_div', div_mul_eq_mul_div_comm → mul_comm_div
• -, mul_div_comm → mul_div_left_comm
• mul_inv, mul_inv₀ → mul_inv
• inv_eq_one, inv_eq_one₀ → inv_eq_one
• one_eq_inv, one_eq_inv₀ → one_eq_inv
• div_div_div_comm, div_div_div_comm₀ → div_div_div_comm
• div_mul_div_comm, div_mul_div_comm₀ → div_mul_div_comm
• mul_div_comm', - → mul_div_mul_comm
• -, div_div_div_div_eq → div_div_div_eq
• one_inv, inv_one → inv_one
• div_div, div_div_eq_div_mul → div_div
• mul_div_left_comm, mul_div_comm → mul_div_left_comm
• div_div_assoc_swap, div_div_eq_mul_div → div_div_eq_mul_div

Other changes

• Arguments order
• Arguments implicitness

---

I found that splitting the refactor in this unusual way allowed me to have a cleaner diff and be systematically sure that I wasn't missing lemmas. The only problem is that I have to unsimp the old lemmas.

Here's what to look out for if you want to check for yourself:

• All lemma renames are either because of the group/group_with_zero disparity or naming consistency within the new API.
• simp and field_simp are copied correctly.
• Every one-lined group/group_with_zero lemma has been deleted.

[Vierkantor]

Impressive work! Everything looks sensible, so let's merge this when it builds.

bors d+

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[bors]

👎 Rejected by label

[YaelDillies]

(We're just waiting for lint and it was already working before the last master merge)

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests