Commit 2020-09-10 14:56 38d1715b

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.