[Merged by Bors] - feat(group_theory/order_of_element): Order in α × β

[YaelDillies]

The order of (a, b) is the lcm of the orders of a and b. Match pow and zpow lemmas. Also some variables noise because I could not use x to mean what I wanted, and incidentally the type A was mostly unused.

---

• depends on: [Merged by Bors] - feat(data/{int,nat}/modeq): a/c ≡ b/c mod m/c → a ≡ b mod m #18666
• depends on: [Merged by Bors] - feat(algebra/group_power/lemmas): Induction principle for powers #18668
• depends on: [Merged by Bors] - feat(algebra/divisibility/basic): Dot notation aliases #18698

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(data/{int,nat}/modeq): a/c ≡ b/c mod m/c → a ≡ b mod m #18666
• [Merged by Bors] - feat(algebra/group_power/lemmas): Induction principle for powers #18668
• [Merged by Bors] - feat(algebra/divisibility/basic): Dot notation aliases #18698
  By Dependent Issues (🤖). Happy coding!

[urkud]

It would be nice to have a lemma about function.minimal_period of prod.map and apply it to order_of. Could you add it, please?

[eric-wieser]

bors d+

Thanks!

[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]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

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