Bump mathlib

YaelDillies · Aug 29, 2024 · 1650046 · 1650046
1 parent 1991985
commit 1650046
Show file tree

Hide file tree

Showing 8 changed files with 5 additions and 46 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -3,15 +3,12 @@ import LeanAPAP.FiniteField.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Action.Defs
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
-import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
-import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.Data.NNReal.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
@@ -20,7 +17,6 @@ import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
-import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC

diff --git a/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean b/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean
diff --git a/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean b/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -10,7 +10,7 @@ lemma norm_one_sub_mul (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ +
     _ ≤ ‖c - a‖ + 1 * ‖1 - b‖ := by gcongr
     _ = ‖c - a‖ + ‖1 - b‖ := by simp
 
-lemma norm_one_sub_mpul' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ := by
+lemma norm_one_sub_mul' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ := by
   rw [add_comm]; exact norm_one_sub_mul (R := Rᵐᵒᵖ) hb
 
 lemma nnnorm_one_sub_mul (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ := norm_one_sub_mul ha

diff --git a/LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean b/LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Order.lean b/LeanAPAP/Mathlib/Data/Fintype/Order.lean
diff --git a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
@@ -20,7 +20,7 @@ lemma energy_nonneg (n : ℕ) (s : Finset G) (ν : G → ℂ) : 0 ≤ energy n s
 lemma energy_nsmul (m n : ℕ) (s : Finset G) (ν : G → ℂ) :
     energy n s (m • ν) = m • energy n s ν := by
   simp only [energy, nsmul_eq_mul, mul_sum, Pi.natCast_def, Pi.mul_apply, norm_mul,
-    Complex.norm_nat]
+    Complex.norm_natCast]
 
 @[simp] lemma energy_zero (s : Finset G) (ν : G → ℂ) : energy 0 s ν = ‖ν 0‖ := by simp [energy]
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "rev": "d38fb94558af9957b8f479e350841ce65a1ec42c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "adaeb6b4d4bf02f60ba3ff6717486a7e895eba77",
+   "rev": "f36af1a7011c102cdf3f5f6c31d2367de28da3a8",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79ef7496100b18304654c1476691e872fa7c491a",
+   "rev": "6ce4187086ef93261927bbc72d061888099b30fc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,