Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-14 16:30 d07245fd

View on Github →

feat(group_theory/order_of_element): Order in α × β (#18719) 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.

Estimated changes