# Commit 2020-09-10 14:56 38d1715b

View on Github →chore(*): update to Lean 3.20.0c, account for nat.pow removal from core (#3985) Outline:

`nat.pow`

has been removed from the core library. We now use the instance`monoid.pow`

to provide`has_pow ℕ ℕ`

.- To accomodate this,
`algebra.group_power`

has been split into a directory.`algebra.group_power.basic`

contains the definitions of`monoid.pow`

and`nsmul`

and whatever lemmas can be stated with very few imports. It is imported in`data.nat.basic`

. The rest of`algebra.group_power`

has moved to`algebra.group_power.lemmas`

. - The new
`has_pow ℕ ℕ`

now satisfies a different definitional equality:`a^(n+1) = a * a^n`

(rather than`a^(n+1) = a^n * a`

). As a temporary measure, the lemma`nat.pow_succ`

provides the old equality but I plan to deprecate it in favor of the more general`pow_succ'`

. The lemma`nat.pow_eq_pow`

is gone--the two sides are now the same in all respects so it can be deleted wherever it was used. - The lemmas from core that mention
`nat.pow`

have been moved into`data.nat.lemmas`

and their proofs adjusted as needed to take into account the new definition. - The module
`data.bitvec`

from core has moved to`data.bitvec.core`

in mathlib. Future plans: - Remove
`nat.`

lemmas redundant with general`group_power`

ones, like`nat.pow_add`

. This will be easier after further shuffling of modules.