Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
commute.is_of_fin_order_mul
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.is_of_fin_order_mul
View on Github →
2022-03-24 05:18
src/group_theory/order_of_element.lean
feat(group_theory/order_of_element): finite orderness is closed under mul (#12750)
Added
commute.is_of_fin_order_mul
View on Github →