chore(*): update to Lean 3.20.0c, account for nat.pow removal from co…

…re (#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>

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.19.0"
+lean_version = "leanprover-community/lean:3.20.0"
 path = "src"
 
 [dependencies]

src/algebra/group_power/basic.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Robert Y. Lewis
+-/
+import algebra.order_functions
+import deprecated.group
+
+/-!
+# Power operations on monoids and groups
+
+The power operation on monoids and groups.
+We separate this from group, because it depends on `ℕ`,
+which in turn depends on other parts of algebra.
+
+This module contains the definitions of `monoid.pow` and `group.pow`
+and their additive counterparts `nsmul` and `gsmul`, along with a few lemmas.
+Further lemmas can be found in `algebra.group_power.lemmas`.
+
+## Notation
+
+The class `has_pow α β` provides the notation `a^b` for powers.
+We define instances of `has_pow M ℕ`, for monoids `M`, and `has_pow G ℤ` for groups `G`.
+
+We also define infix operators `•ℕ` and `•ℤ` for scalar multiplication by a natural and an integer
+numbers, respectively.
+
+## Implementation details
+
+We adopt the convention that `0^0 = 1`.
+
+This module provides the instance `has_pow ℕ ℕ` (via `monoid.has_pow`)
+and is imported by `data.nat.basic`, so it has to live low in the import hierarchy.
+Not all of its imports are needed yet; the intent is to move more lemmas here from `.lemmas`
+so that they are available in `data.nat.basic`, and the imports will be required then.
+-/
+
+universes u v w x y z u₁ u₂
+
+variables {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
+  {R : Type u₁} {S : Type u₂}
+
+/-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
+def monoid.pow [has_mul M] [has_one M] (a : M) : ℕ → M
+| 0     := 1
+| (n+1) := a * monoid.pow n
+
+/-- The scalar multiplication in an additive monoid.
+`n •ℕ a = a+a+...+a` n times. -/
+def nsmul [has_add A] [has_zero A] (n : ℕ) (a : A) : A :=
+@monoid.pow (multiplicative A) _ { one := (0 : A) } a n
+
+infix ` •ℕ `:70 := nsmul
+
+@[priority 5] instance monoid.has_pow [monoid M] : has_pow M ℕ := ⟨monoid.pow⟩
+
+/-!
+### Commutativity
+
+First we prove some facts about `semiconj_by` and `commute`. They do not require any theory about
+`pow` and/or `nsmul` and will be useful later in this file.
+-/
+
+namespace semiconj_by
+
+variables [monoid M]
+
+@[simp] lemma pow_right {a x y : M} (h : semiconj_by a x y) (n : ℕ) : semiconj_by a (x^n) (y^n) :=
+nat.rec_on n (one_right a) $ λ n ihn, h.mul_right ihn
+
+end semiconj_by
+
+namespace commute
+
+variables [monoid M] {a b : M}
+
+@[simp] theorem pow_right (h : commute a b) (n : ℕ) : commute a (b ^ n) := h.pow_right n
+@[simp] theorem pow_left (h : commute a b) (n : ℕ) : commute (a ^ n) b := (h.symm.pow_right n).symm
+@[simp] theorem pow_pow (h : commute a b) (m n : ℕ) : commute (a ^ m) (b ^ n) :=
+(h.pow_left m).pow_right n
+
+@[simp] theorem self_pow (a : M) (n : ℕ) : commute a (a ^ n) := (commute.refl a).pow_right n
+@[simp] theorem pow_self (a : M) (n : ℕ) : commute (a ^ n) a := (commute.refl a).pow_left n
+@[simp] theorem pow_pow_self (a : M) (m n : ℕ) : commute (a ^ m) (a ^ n) :=
+(commute.refl a).pow_pow m n
+
+end commute
+
+section monoid
+variables [monoid M] [monoid N] [add_monoid A] [add_monoid B]
+
+@[simp] theorem pow_zero (a : M) : a^0 = 1 := rfl
+@[simp] theorem zero_nsmul (a : A) : 0 •ℕ a = 0 := rfl
+
+theorem pow_succ (a : M) (n : ℕ) : a^(n+1) = a * a^n := rfl
+theorem succ_nsmul (a : A) (n : ℕ) : (n+1) •ℕ a = a + n •ℕ a := rfl
+
+theorem pow_two (a : M) : a^2 = a * a :=
+show a*(a*1)=a*a, by rw mul_one
+theorem two_nsmul (a : A) : 2 •ℕ a = a + a :=
+@pow_two (multiplicative A) _ a
+
+theorem pow_mul_comm' (a : M) (n : ℕ) : a^n * a = a * a^n := commute.pow_self a n
+theorem nsmul_add_comm' : ∀ (a : A) (n : ℕ), n •ℕ a + a = a + n •ℕ a :=
+@pow_mul_comm' (multiplicative A) _
+
+theorem pow_succ' (a : M) (n : ℕ) : a^(n+1) = a^n * a :=
+by rw [pow_succ, pow_mul_comm']
+theorem succ_nsmul' (a : A) (n : ℕ) : (n+1) •ℕ a = n •ℕ a + a :=
+@pow_succ' (multiplicative A) _ _ _
+
+theorem pow_add (a : M) (m n : ℕ) : a^(m + n) = a^m * a^n :=
+by induction n with n ih; [rw [nat.add_zero, pow_zero, mul_one],
+  rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', nat.add_assoc]]
+theorem add_nsmul : ∀ (a : A) (m n : ℕ), (m + n) •ℕ a = m •ℕ a + n •ℕ a :=
+@pow_add (multiplicative A) _
+
+end monoid
+
+section group
+variables [group G] [group H] [add_group A] [add_group B]
+
+open int
+
+/--
+The power operation in a group. This extends `monoid.pow` to negative integers
+with the definition `a^(-n) = (a^n)⁻¹`.
+-/
+def gpow (a : G) : ℤ → G
+| (of_nat n) := a^n
+| -[1+n]     := (a^(nat.succ n))⁻¹
+
+/--
+The scalar multiplication by integers on an additive group.
+This extends `nsmul` to negative integers
+with the definition `(-n) •ℤ a = -(n •ℕ a)`.
+-/
+def gsmul (n : ℤ) (a : A) : A :=
+@gpow (multiplicative A) _ a n
+
+@[priority 10] instance group.has_pow : has_pow G ℤ := ⟨gpow⟩
+
+infix ` •ℤ `:70 := gsmul
+
+end group

src/algebra/group_power/default.lean

@@ -0,0 +1 @@
+import algebra.group_power.lemmas

src/algebra/group_power.lean → src/algebra/group_power/lemmas.lean

@@ -3,101 +3,31 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
+import algebra.group_power.basic
 import algebra.opposites
 import data.list.basic
 import data.int.cast
 import data.equiv.basic
 import deprecated.group
 
 /-!
-# Power operations on monoids and groups
+# Lemmas about power operations on monoids and groups
 
-The power operation on monoids and groups.
-We separate this from group, because it depends on `ℕ`,
-which in turn depends on other parts of algebra.
-
-## Notation
-
-The class `has_pow α β` provides the notation `a^b` for powers.
-We define instances of `has_pow M ℕ`, for monoids `M`, and `has_pow G ℤ` for groups `G`.
-
-We also define infix operators `•ℕ` and `•ℤ` for scalar multiplication by a natural and an integer
-numbers, respectively.
-
-## Implementation details
-
-We adopt the convention that `0^0 = 1`.
+This file contains lemmas about `monoid.pow`, `group.pow`, `nsmul`, `gsmul`
+which require additional imports besides those available in `.basic`.
 -/
 
 universes u v w x y z u₁ u₂
 
 variables {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
   {R : Type u₁} {S : Type u₂}
 
-/-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
-def monoid.pow [has_mul M] [has_one M] (a : M) : ℕ → M
-| 0     := 1
-| (n+1) := a * monoid.pow n
-
-/-- The scalar multiplication in an additive monoid.
-`n •ℕ a = a+a+...+a` n times. -/
-def nsmul [has_add A] [has_zero A] (n : ℕ) (a : A) : A :=
-@monoid.pow (multiplicative A) _ { one := (0 : A) } a n
-
-infix ` •ℕ `:70 := nsmul
-
-@[priority 5] instance monoid.has_pow [monoid M] : has_pow M ℕ := ⟨monoid.pow⟩
-
-/-!
-### Commutativity
-
-First we prove some facts about `semiconj_by` and `commute`. They do not require any theory about
-`pow` and/or `nsmul` and will be useful later in this file.
--/
-
-namespace semiconj_by
-
-variables [monoid M]
-
-@[simp] lemma pow_right {a x y : M} (h : semiconj_by a x y) (n : ℕ) : semiconj_by a (x^n) (y^n) :=
-nat.rec_on n (one_right a) $ λ n ihn, h.mul_right ihn
-
-end semiconj_by
-
-namespace commute
-
-variables [monoid M] {a b : M}
-
-@[simp] theorem pow_right (h : commute a b) (n : ℕ) : commute a (b ^ n) := h.pow_right n
-
-@[simp] theorem pow_left (h : commute a b) (n : ℕ) : commute (a ^ n) b := (h.symm.pow_right n).symm
-
-@[simp] theorem pow_pow (h : commute a b) (m n : ℕ) : commute (a ^ m) (b ^ n) :=
-(h.pow_left m).pow_right n
-
-@[simp] theorem self_pow (a : M) (n : ℕ) : commute a (a ^ n) := (commute.refl a).pow_right n
-
-@[simp] theorem pow_self (a : M) (n : ℕ) : commute (a ^ n) a := (commute.refl a).pow_left n
-
-@[simp] theorem pow_pow_self (a : M) (m n : ℕ) : commute (a ^ m) (a ^ n) :=
-(commute.refl a).pow_pow m n
-
-end commute
-
 /-!
 ### (Additive) monoid
 -/
 section monoid
 variables [monoid M] [monoid N] [add_monoid A] [add_monoid B]
 
-@[simp] theorem pow_zero (a : M) : a^0 = 1 := rfl
-
-@[simp] theorem zero_nsmul (a : A) : 0 •ℕ a = 0 := rfl
-
-theorem pow_succ (a : M) (n : ℕ) : a^(n+1) = a * a^n := rfl
-
-theorem succ_nsmul (a : A) (n : ℕ) : (n+1) •ℕ a = a + n •ℕ a := rfl
-
 @[simp] theorem pow_one (a : M) : a^1 = a := mul_one _
 
 @[simp] theorem one_nsmul (a : A) : 1 •ℕ a = a := add_zero _
@@ -114,30 +44,6 @@ by split_ifs; refl
   a ^ (if P then 1 else 0) = if P then a else 1 :=
 by simp
 
-theorem pow_mul_comm' (a : M) (n : ℕ) : a^n * a = a * a^n := commute.pow_self a n
-
-theorem nsmul_add_comm' : ∀ (a : A) (n : ℕ), n •ℕ a + a = a + n •ℕ a :=
-@pow_mul_comm' (multiplicative A) _
-
-theorem pow_succ' (a : M) (n : ℕ) : a^(n+1) = a^n * a :=
-by rw [pow_succ, pow_mul_comm']
-
-theorem succ_nsmul' (a : A) (n : ℕ) : (n+1) •ℕ a = n •ℕ a + a :=
-@pow_succ' (multiplicative A) _ _ _
-
-theorem pow_two (a : M) : a^2 = a * a :=
-show a*(a*1)=a*a, by rw mul_one
-
-theorem two_nsmul (a : A) : 2 •ℕ a = a + a :=
-@pow_two (multiplicative A) _ a
-
-theorem pow_add (a : M) (m n : ℕ) : a^(m + n) = a^m * a^n :=
-by induction n with n ih; [rw [add_zero, pow_zero, mul_one],
-  rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', add_assoc]]
-
-theorem add_nsmul : ∀ (a : A) (m n : ℕ), (m + n) •ℕ a = m •ℕ a + n •ℕ a :=
-@pow_add (multiplicative A) _
-
 @[simp] theorem one_pow (n : ℕ) : (1 : M)^n = 1 :=
 by induction n with n ih; [refl, rw [pow_succ, ih, one_mul]]
 
@@ -228,10 +134,6 @@ theorem neg_pow [ring R] (a : R) (n : ℕ) : (- a) ^ n = (-1) ^ n * a ^ n :=
 
 end monoid
 
-@[simp] theorem nat.pow_eq_pow (p q : ℕ) :
-  @has_pow.pow _ _ monoid.has_pow p q = p ^ q :=
-by induction q with q ih; [refl, rw [nat.pow_succ, pow_succ', ih]]
-
 theorem nat.nsmul_eq_mul (m n : ℕ) : m •ℕ n = m * n :=
 by induction m with m ih; [rw [zero_nsmul, zero_mul],
   rw [succ_nsmul', ih, nat.succ_mul]]
@@ -291,26 +193,6 @@ end nat
 
 open int
 
-/--
-The power operation in a group. This extends `monoid.pow` to negative integers
-with the definition `a^(-n) = (a^n)⁻¹`.
--/
-def gpow (a : G) : ℤ → G
-| (of_nat n) := a^n
-| -[1+n]     := (a^(nat.succ n))⁻¹
-
-/--
-The scalar multiplication by integers on an additive group.
-This extends `nsmul` to negative integers
-with the definition `(-n) •ℤ a = -(n •ℕ a)`.
--/
-def gsmul (n : ℤ) (a : A) : A :=
-@gpow (multiplicative A) _ a n
-
-@[priority 10] instance group.has_pow : has_pow G ℤ := ⟨gpow⟩
-
-infix ` •ℤ `:70 := gsmul
-
 @[simp] theorem gpow_coe_nat (a : G) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl
 
 @[simp] theorem gsmul_coe_nat (a : A) (n : ℕ) : n •ℤ a = n •ℕ a := rfl

src/analysis/specific_limits.lean

@@ -160,11 +160,8 @@ sub_add_cancel r 1 ▸ tendsto_add_one_pow_at_top_at_top_of_pos (sub_pos.2 h)
 
 lemma nat.tendsto_pow_at_top_at_top_of_one_lt {m : ℕ} (h : 1 < m) :
   tendsto (λn:ℕ, m ^ n) at_top at_top :=
-begin
-  simp only [← nat.pow_eq_pow],
-  exact nat.sub_add_cancel (le_of_lt h) ▸
-    tendsto_add_one_pow_at_top_at_top_of_pos (nat.sub_pos_of_lt h)
-end
+nat.sub_add_cancel (le_of_lt h) ▸
+  tendsto_add_one_pow_at_top_at_top_of_pos (nat.sub_pos_of_lt h)
 
 lemma lim_norm_zero' {𝕜 : Type*} [normed_group 𝕜] :
   tendsto (norm : 𝕜 → ℝ) (𝓝[{x | x ≠ 0}] 0) (𝓝[set.Ioi 0] 0) :=

src/data/bitvec/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Simon Hudon
 -/
-import data.bitvec
+import data.bitvec.core
 import data.fin
 import tactic.norm_num
 import tactic.monotonicity