This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
[Merged by Bors] - refactor(algebra/{group,group_with_zero/basic): Generalize lemmas to division monoids #14000
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Generalize
group
andgroup_with_zero
lemmas todivision_monoid
. We do not actually delete the original lemmas but make them one-liners from the new ones. The next PR will then delete the old lemmas and perform the renames in all files.Lemmas are renamed because
group
orgroup_with_zero
name has to goPre-emptive lemma renames
group
lemma,group_with_zero
lemma → newdivision_monoid
/division_comm_monoid
lemmainv_eq_of_mul_eq_one
,inv_eq_of_mul_left_eq_one
→inv_eq_of_mul_eq_one_left
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
mul_comm_div'
,div_mul_eq_mul_div_comm
→mul_comm_div
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
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
left_inverse_inv
andright_inverse_inv
tohas_involutive_inv
, anddiv_eq_mul_one_div
todiv_inv_monoid
.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:
group
/group_with_zero
disparity or naming consistency within the new API.simp
andfield_simp
are copied correctly.group
/group_with_zero
lemma in the two files has been one-lined (some in other files haven't, but I will take care of them in another PR.division_monoid
lemma is used to one-line an old lemma.