# Commit 2024-05-13 11:45 cec3ec0b

View on Github →chore: Delete `Algebra.GroupWithZero.Power`

(#12825)
After #12736, all lemmas in `Algebra.GroupWithZero.Power`

can move to the earlier files where they belong. The changes to their proofs are minimal. It's just a matter of using the new Lean 4 `Nat`

- and `Int`

-specific lemmas instead of the generic algebraic order ones.