mathlib

38d1715b - chore(*): update to Lean 3.20.0c, account for nat.pow removal from core (#3985)

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. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>