chore: bump to v4.22.0 (#306)

Author: pitmonticone

MIL/C09_Groups_and_Rings/S02_Rings.lean

@@ -1,7 +1,6 @@
 -- BOTH:
 import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Localization.Basic
-import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.Analysis.Complex.Polynomial.Basic
 import Mathlib.Data.ZMod.QuotientRing
 import MIL.Common

MIL/C10_Linear_Algebra/S02_Subspaces.lean

@@ -204,7 +204,7 @@ example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.
   (h.submodule_iSupIndep.pairwiseDisjoint hij).eq_bot
 
 -- Those conditions characterize direct sums.
-#check DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top
+#check DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top
 
 -- The relation with external direct sums: if a family of subspaces is
 -- in internal direct sum then the map from their external direct sum into `V`

MIL/C10_Linear_Algebra/S04_Bases.lean

@@ -254,6 +254,8 @@ variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
 
 section
 
+open Module
+
 variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)
 
 -- The basis vector with index ``i``
@@ -501,6 +503,7 @@ since a given abelian group can be a vector space over different fields.
 EXAMPLES: -/
 -- QUOTE:
 section
+
 #check (Module.finrank K V : ℕ)
 
 -- `Fin n → K` is the archetypical space with dimension `n` over `K`.
@@ -553,7 +556,7 @@ is good to know for more complicated cases.
 By definition, ``FiniteDimensional K V`` can be read from any basis.
 EXAMPLES: -/
 -- QUOTE:
-variable {ι : Type*} (B : Basis ι K V)
+variable {ι : Type*} (B : Module.Basis ι K V)
 
 example [Finite ι] : FiniteDimensional K V := FiniteDimensional.of_fintype_basis B
 
@@ -660,8 +663,8 @@ EXAMPLES: -/
 
 universe u v -- `u` and `v` will denote universe levels
 
-variable {ι : Type u} (B : Basis ι K V)
-         {ι' : Type v} (B' : Basis ι' K V)
+variable {ι : Type u} (B : Module.Basis ι K V)
+         {ι' : Type v} (B' : Module.Basis ι' K V)
 
 example : Cardinal.lift.{v, u} (.mk ι) = Cardinal.lift.{u, v} (.mk ι') :=
   mk_eq_mk_of_basis B B'

lake-manifest.json

@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.62",
+   "inputRev": "v0.0.68",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -9,7 +9,7 @@ relaxedAutoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.21.0"
+rev = "v4.22.0"
 
 [[lean_lib]]
 name = "MIL"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0
+leanprover/lean4:v4.22.0