Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 11:06 cd196a8a

View on Github →

feat(group_theory/order_of_element): 1 is finite order, as is g⁻¹ (#12749)

Estimated changes

added theorem is_of_fin_order_inv
added theorem is_of_fin_order_one