Upgrade Lean and mathlib

leanpkg.toml

@@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.50.3"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d1723c047a091ae3fca0af8aeab1743e1a898611"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5aa3c1de9f3c642eac76e11071c852766f220fd0"}

src/demos/category_theory.lean

@@ -1,5 +1,5 @@
 import category_theory.category.basic
-import category_theory.functor
+import category_theory.functor.basic
 
 import algebra.category.Group.images
 import algebra.category.Group.colimits
@@ -11,7 +11,7 @@ import category_theory.abelian.basic
 import category_theory.limits.shapes.finite_limits
 
 import topology.instances.real
-import topology.category.Top
+import topology.category.Top.limits
 import topology.category.UniformSpace
 
 

src/demos/linalg.lean

@@ -1,4 +1,4 @@
-import algebra.module
+import algebra.module.basic
 import analysis.inner_product_space.basic
 import data.matrix.notation
 import data.matrix.dmatrix
@@ -213,14 +213,14 @@ are `fintype`s, and there is no restriction on the type `α` of the entries.
 Like vectors in `n → R`, matrices are typically indexed over `fin k`.
 To define a matrix, you map the indexes to the entry:
 -/
-def example_matrix : matrix (fin 2) (fin 3) ℤ := λ i j, i + j
+def example_matrix : matrix (fin 2) (fin 3) ℤ := matrix.of (λ i j, (↑i + ↑j : ℤ))
 #eval example_matrix 1 2
 
-/- Like vectors, we can use `![...]` notation to define matrices: -/
+/- Simiilarly to vectors, we can use `!![...]` notation to define matrices: -/
 def other_example_matrix : matrix (fin 3) (fin 2) ℤ :=
-![![0, 1],
-  ![1, 2],
-  ![2, 3]]
+!![0, 1;
+   1, 2;
+   2, 3]
 
 /- We have the 0 matrix and the sum of two matrices: -/
 example (i j) : (0 : matrix m n R) i j = 0 := dmatrix.zero_apply i j
@@ -262,7 +262,7 @@ as long as you have chosen a basis for each module.
 -/
 variables [decidable_eq m] [decidable_eq n]
 variables (v : basis m R M) (w : basis n R N)
-#check linear_map.to_matrix v w -- (M →ₗ[R] N) ≈ₗ[R] matrix n m R
+#check linear_map.to_matrix v w -- (M →ₗ[R] N) ≃ₗ[R] matrix n m R
 
 /-
 Invertible (i.e. nonsingular) matrices have an inverse operation denoted by `⁻¹`.

src/exercises_sources/friday/analysis.lean

@@ -14,7 +14,7 @@ namespace lftcm
 noncomputable theory
 
 open real
-open_locale topological_space filter classical real
+open_locale topology filter classical real
 
 /-!
 # Derivatives

src/exercises_sources/friday/topology.lean

@@ -1,6 +1,6 @@
 import topology.metric_space.basic
 
-open_locale classical filter topological_space
+open_locale classical filter topology
 
 namespace lftcm
 open filter set

src/exercises_sources/thursday/category_theory/exercise2.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 /-!
 Let's show that taking polynomials over a ring is functor `Ring ⥤ Ring`.

src/exercises_sources/thursday/category_theory/exercise4.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/exercises_sources/thursday/groups_rings_fields.lean

@@ -2,6 +2,7 @@ import linear_algebra.finite_dimensional
 import ring_theory.algebraic
 import data.zmod.basic
 import data.real.basic
+import data.nat.choose.dvd
 import tactic
 
 /-!

src/exercises_sources/thursday/linear_algebra.lean

@@ -1,7 +1,6 @@
 import analysis.inner_product_space.basic
 import data.matrix.notation
 import linear_algebra.bilinear_form
-import linear_algebra.matrix
 import tactic
 
 universes u v
@@ -166,10 +165,13 @@ Hints:
 * Try the lemmas `finset.sum_nonneg`, `finset.sum_eq_zero_iff_of_nonneg`,
   `mul_self_nonneg` and `mul_self_eq_zero`.
 -/
-noncomputable instance : inner_product_space ℝ (n → ℝ) :=
-inner_product_space.of_core
+noncomputable instance : normed_add_comm_group (n → ℝ):=
+@inner_product_space.of_core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
 sorry
 
+noncomputable instance : inner_product_space ℝ (n → ℝ) :=
+inner_product_space.of_core _
+
 end pi
 
 end exercise3

src/exercises_sources/tuesday/sets.lean

@@ -1,4 +1,5 @@
 import data.set.basic data.set.lattice data.nat.parity
+import data.nat.prime
 import tactic.linarith
 
 open set nat function

src/for_mathlib/manifolds.lean

@@ -21,7 +21,7 @@ include hp
 lemma pi_Lp.norm_coord_le_norm (x : pi_Lp p α) (i : ι) : ‖x i‖ ≤ ‖x‖ :=
 begin
   unfreezingI { rcases p.trichotomy with (rfl | rfl | h) },
-  { exact false.elim (lt_irrefl _ (ennreal.zero_lt_one.trans_le hp.out)) },
+  { exact false.elim (lt_irrefl _ (zero_lt_one.trans_le hp.out)) },
   { rw pi_Lp.norm_eq_csupr,
     exact le_cSup (finite_range _).bdd_above (mem_range_self _) },
   { calc
@@ -74,7 +74,7 @@ begin
     begin
       refine (F i).mk_continuous 1 (λ x, _),
       unfreezingI { rcases p.trichotomy with (rfl | rfl | h) },
-      { exact false.elim (lt_irrefl _ (ennreal.zero_lt_one.trans_le hp.out)) },
+      { exact false.elim (lt_irrefl _ (zero_lt_one.trans_le hp.out)) },
       { haveI : nonempty ι := ⟨i⟩,
         simp only [pi_Lp.norm_eq_csupr, linear_map.coe_mk, one_mul],
         refine cSup_le (range_nonempty _) _,

src/hints/category_theory/exercise2/hint1.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint2.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint3.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint4.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint5.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint6.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint7.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise4/hint1.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/hints/category_theory/exercise4/hint2.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/hints/category_theory/exercise4/hint3.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/hints/category_theory/exercise4/hint4.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/solutions/friday/topology.lean

@@ -1,6 +1,6 @@
 import topology.metric_space.basic
 
-open_locale classical filter topological_space
+open_locale classical filter topology
 
 namespace lftcm
 open filter set

src/solutions/thursday/category_theory/exercise2.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 /-!
 Let's show that taking polynomials over a ring is functor `Ring ⥤ Ring`.

src/solutions/thursday/category_theory/exercise4.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/solutions/thursday/groups_rings_fields.lean

@@ -2,6 +2,7 @@ import linear_algebra.finite_dimensional
 import ring_theory.algebraic
 import data.zmod.basic
 import data.real.basic
+import data.nat.choose.dvd
 import tactic
 
 /-!
@@ -292,8 +293,7 @@ begin
   { intros i hi hi0,
     convert mul_zero _,
     rw char_p.cast_eq_zero_iff K p,
-    apply nat.prime.dvd_choose_self _ _ (fact.out p.prime),
-    { rwa pos_iff_ne_zero },
+    apply nat.prime.dvd_choose_self (fact.out p.prime) hi0 _,
     { simpa using hi } },
   { intro h,
     simp only [le_zero_iff, mem_range, not_lt] at h,

src/solutions/thursday/linear_algebra.lean

@@ -1,7 +1,6 @@
 import analysis.inner_product_space.basic
 import data.matrix.notation
 import linear_algebra.bilinear_form
-import linear_algebra.matrix
 import tactic
 
 universes u v
@@ -235,18 +234,21 @@ Hints:
 * Try the lemmas `finset.sum_nonneg`, `finset.sum_eq_zero_iff_of_nonneg`,
   `mul_self_nonneg` and `mul_self_eq_zero`.
 -/
-noncomputable instance : inner_product_space ℝ (n → ℝ) :=
-inner_product_space.of_core
+noncomputable instance : normed_add_comm_group (n → ℝ):=
+@inner_product_space.of_core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
 -- sorry
 { inner := dot_product,
   nonneg_re := λ x, finset.sum_nonneg (λ i _, mul_self_nonneg _),
   definite := λ x hx, funext (λ i, mul_self_eq_zero.mp
     ((finset.sum_eq_zero_iff_of_nonneg (λ i _, mul_self_nonneg (x i))).mp hx i (finset.mem_univ i))),
-  conj_sym := λ x y, dot_product_comm _ _,
+  conj_symm := λ x y, dot_product_comm _ _,
   add_left := λ x y z, add_dot_product _ _ _,
   smul_left := λ s x y, smul_dot_product _ _ _ }
 -- sorry
 
+noncomputable instance : inner_product_space ℝ (n → ℝ) :=
+inner_product_space.of_core _
+
 end pi
 
 end exercise3

src/solutions/tuesday/numbers.lean

@@ -1,7 +1,7 @@
 import tactic
 import data.real.basic
 import data.int.gcd
-import number_theory.padics
+import number_theory.padics.padic_numbers
 import data.nat.prime_norm_num
 
 /-!

src/solutions/tuesday/sets.lean

@@ -1,4 +1,5 @@
 import data.set.basic data.set.lattice data.nat.parity
+import data.nat.prime
 import tactic.linarith
 
 open set nat function