Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-18 01:02 0ff11df2

View on Github →

refactor(group_theory/order_of_element): use gpowers instead of range (#265)

Estimated changes

modified theorem exists_pow_eq_one
added theorem order_eq_card_gpowers
deleted theorem order_eq_card_range_gpow
deleted theorem order_of_ne_zero
added theorem order_of_pos