mathlib3
792d3e56 - feat(group_theory/order_of_element): pow_eq_pow_iff_modeq (#11737)

Commit

4 years ago

feat(group_theory/order_of_element): pow_eq_pow_iff_modeq (#11737) From flt-regular. Co-authored-by: Johan Commelin <johan@commelin.net>

Author

ericrbg

Parents