mathlib3
5118ae32 - feat(algebra/group_power/order): add `pow_lt_self_of_lt_one` (#17162)

Commit

3 years ago

feat(algebra/group_power/order): add `pow_lt_self_of_lt_one` (#17162)

Author

urkud

urkud

Parents

Loading