Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-24 05:18
ec434b75
View on Github →
feat(group_theory/order_of_element): finite orderness is closed under mul (
#12750
)
Estimated changes
Modified
src/group_theory/order_of_element.lean
added
theorem
commute.is_of_fin_order_mul
added
theorem
is_of_fin_order.inv
added
theorem
is_of_fin_order.mul
deleted
theorem
is_of_fin_order_inv
added
theorem
order_of_pos_iff