Theorem commute.order_of_mul_dvd_lcm
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_dvd_lcmView on Github →2021-12-14 09:33
src/group_theory/order_of_element.lean
feat(group_theory/order_of_element): additivize (#10766)
Modified commute.order_of_mul_dvd_lcmView on Github →