mathlib

17c74f19 - feat(algebra/group_power/order): add le_pow (#12436)

feat(algebra/group_power/order): add le_pow (#12436) Added a new theorem so that library search will find it. Co-authored-by: seangolinski7 <60711021+seangolinski7@users.noreply.github.com>