Mathlib v3 is deprecated. Go to Mathlib v4

Theorem commute.order_of_mul_eq_mul_order_of_of_coprime

Modification history

2022-12-22 09:08
src/group_theory/order_of_element.lean
feat(group_theory/order_of_element): a condition on o(x) and o(y) that implies o(xy)=o(y) (#17997) …
Modified commute.order_of_mul_eq_mul_order_of_of_coprimeView on Github →
2021-12-04 00:14
src/group_theory/order_of_element.lean
feat(group_theory/order_of_element): order of a product of elements (#10399) …
Added commute.order_of_mul_eq_mul_order_of_of_coprimeView on Github →