[Merged by Bors] - chore: Rename `mul`-`div` cancellation lemmas by YaelDillies · Pull Request #11530 · leanprover-community/mathlib4

YaelDillies · 2024-03-20T11:44:18Z

Lemma names around cancellation of multiplication and division are a mess.

This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the GroupWithZero lemma name, the Group lemma, the AddGroup lemma name).

Statement	New name	Old name
`(a * b) / a = b`	`mul_div_cancel_left₀`	`mul_div_cancel_left`
	`mul_div_cancel_left`	`mul_div_cancel'''`
	`add_sub_cancel_left`	`add_sub_cancel'`
`(a * b) / b = a`	`mul_div_cancel_right₀`	`mul_div_cancel`
	`mul_div_cancel_right`	`mul_div_cancel''`
	`add_sub_cancel_right`	`add_sub_cancel`
`a / (a * b) = b⁻¹`	`div_mul_cancel_left₀`	`div_mul_right` (roughly)
	`div_mul_cancel_left`	`div_mul_cancel''`
	`sub_add_cancel_left`	`sub_add_cancel'`
`b / (a * b) = a⁻¹`	`div_mul_cancel_right₀`	`div_mul_left` (roughly)
	`div_mul_cancel_right`	`div_mul_cancel'''`
	`sub_add_cancel_right`	`sub_add_cancel''`
`a * (b / a) = b`	`mul_div_cancel₀`	`mul_div_cancel'`
	`mul_div_cancel`	`mul_div_cancel'_right`
	`add_sub_cancel`	`add_sub_cancel'_right`
`(a / b) * b = a`	`div_mul_cancel₀`	`div_mul_cancel`
	`div_mul_cancel`	`div_mul_cancel'`
	`sub_add_cancel`	`sub_add_cancel`

Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |---------------------|-------------------------|-------------------------| | `(a * b) / a = b` | `mul_div_eq_right₀` | `mul_div_cancel_left` | | | `mul_div_eq_right` | `mul_div_cancel'''` | | | `add_sub_eq_right` | `add_sub_cancel'` | | `(a * b) / b = a` | `mul_div_eq_left₀` | `mul_div_cancel` | | | `mul_div_eq_left` | `mul_div_cancel''` | | | `add_sub_eq_left` | `add_sub_cancel` | | `a / (a * b) = b⁻¹` | `div_mul_eq_inv_right₀` | roughly `div_mul_right` | | | `div_mul_eq_inv_right` | `div_mul_cancel''` | | | `sub_add_eq_neg_right` | `sub_add_cancel'` | | `a / (a * b) = a⁻¹` | `div_mul_eq_inv_left₀` | roughly `div_mul_left` | | | `div_mul_eq_inv_left` | `div_mul_cancel'''` | | | `sub_add_eq_neg_left` | `sub_add_cancel''` | | `a * (b / a) = b` | `mul_div_cancel₀` | `mul_div_cancel'` | | | `mul_div_cancel` | `mul_div_cancel'_right` | | | `add_sub_cancel` | `add_sub_cancel'_right` | | `(a / b) * b = a` | `div_mul_cancel₀` | `div_mul_cancel` | | | `div_mul_cancel` | `div_mul_cancel'` | | | `sub_add_cancel` | `sub_add_cancel` |

fpvandoorn · 2024-03-20T12:47:23Z

For these kinds of basic lemma renames, it might be good to make a Zulip thread with the suggested renames, and only do it if nobody makes a major objection for 1-2 days.
Some of the old names matched the naming of mul_inv_cancel_right + siblings (mul_inv_cancel_left, inv_mul_cancel_left, inv_mul_cancel_right).

That said, this is definitely an improvement over all the primed lemmas. However, it's a bit unfortunate that in the new naming scheme the GroupWithZero lemmas don't have the "default name" anymore, since they are the more commonly used ones.

YaelDillies · 2024-03-20T13:57:23Z

Zulip

fpvandoorn · 2024-03-20T21:33:24Z

Second Zulip thread for more visibility. I'm happy to merge this in ~24 hours if there is no serious criticism.

fpvandoorn · 2024-03-22T08:31:16Z

I think the rename I suggested is popular. If you change the names to that naming scheme, then I'll merge/delegate this.

fpvandoorn · 2024-03-23T13:19:51Z

LGTM. I didn't have time yesterday to look at this again, so hopefully there are not conflicts.

bors merge (let's try, but I'm not too hopeful)
bors d+

mathlib-bors · 2024-03-23T13:19:53Z

✌️ 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.

Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |

mathlib-bors · 2024-03-23T14:14:12Z

Build failed:

Build

This is fallout from #11530. Somehow CI didn't catch that.

We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>