Bump mathlib

LeanAPAP.lean

@@ -1,13 +1,11 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
 import LeanAPAP.Mathlib.Algebra.BigOperators.Basic
-import LeanAPAP.Mathlib.Algebra.BigOperators.Order
 import LeanAPAP.Mathlib.Algebra.BigOperators.Pi
 import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.Order.Field.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Group.Abs
 import LeanAPAP.Mathlib.Algebra.Order.Group.PosPart
-import LeanAPAP.Mathlib.Algebra.Star.Order
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Analysis.MeanInequalities
 import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
@@ -18,7 +16,6 @@ import LeanAPAP.Mathlib.Data.Complex.Order
 import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Fintype.Pi
 import LeanAPAP.Mathlib.Data.NNRat.Defs
-import LeanAPAP.Mathlib.Data.Rat.Order
 import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Mathlib.Data.ZMod.Basic
 import LeanAPAP.Mathlib.GroupTheory.GroupAction.BigOperators

LeanAPAP/Extras/BSG.lean

@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Algebra.BigOperators.Order
 import LeanAPAP.Mathlib.Combinatorics.Additive.Energy
 import LeanAPAP.Prereqs.Discrete.Convolution.Order
 

LeanAPAP/Mathlib/GroupTheory/Submonoid/Operations.lean

@@ -1,7 +1,4 @@
-import Mathlib.Algebra.Parity
-import Mathlib.Algebra.GroupWithZero.Power
 import Mathlib.GroupTheory.Submonoid.Operations
-import LeanAPAP.Mathlib.Data.Rat.Order
 
 namespace Submonoid
 variable {M : Type*} [MulOneClass M] {S : Submonoid M}
@@ -10,36 +7,3 @@ variable {M : Type*} [MulOneClass M] {S : Submonoid M}
 lemma mk_eq_one {a : M} {ha} : (⟨a, ha⟩ : S) = 1 ↔ a = 1 := by simp [← SetLike.coe_eq_coe]
 
 end Submonoid
-
-open AddSubmonoid Set
-
-namespace Nat
-
-@[simp] lemma addSubmonoid_closure_one : closure ({1} : Set ℕ) = ⊤ := by
-  refine' (eq_top_iff' _).2 (Nat.rec _ _)
-  · exact zero_mem _
-  · simp_rw [Nat.succ_eq_add_one]
-    exact fun n hn ↦ AddSubmonoid.add_mem _ hn (subset_closure $ Set.mem_singleton _)
-
-end Nat
-
-namespace Rat
-
-@[simp] lemma addSubmonoid_closure_range_pow {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) :
-    closure (range fun x : ℚ ↦ x ^ n) = nonneg _ := by
-  refine' le_antisymm (closure_le.2 $ range_subset_iff.2 hn.pow_nonneg) fun x hx ↦ _
-  suffices x = (x.num.natAbs * x.den ^ (n - 1)) • (x.den : ℚ)⁻¹ ^ n by
-    rw [this]
-    exact nsmul_mem (subset_closure $ mem_range_self _) _
-  rw [nsmul_eq_mul]
-  push_cast
-  rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel, one_pow, one_mul,
-    ← Int.cast_ofNat, Int.coe_natAbs, abs_of_nonneg, ← div_eq_mul_inv, num_div_den]
-  rw [mem_nonneg] at hx
-  all_goals simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]
-
-@[simp]
-lemma addSubmonoid_closure_range_mul_self : closure (range fun x : ℚ ↦ x * x) = nonneg _ := by
-  simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero even_two
-
-end Rat

LeanAPAP/Physics/Unbalancing.lean

@@ -1,5 +1,4 @@
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Algebra.BigOperators.Order
 import LeanAPAP.Mathlib.Algebra.Order.Field.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Group.PosPart
 import LeanAPAP.Mathlib.Data.Complex.Order

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -1,5 +1,6 @@
 import Mathlib.GroupTheory.FiniteAbelian
 import LeanAPAP.Mathlib.Data.ZMod.Basic
+import LeanAPAP.Mathlib.GroupTheory.Submonoid.Operations
 import LeanAPAP.Prereqs.AddChar.Circle
 
 /-!

LeanAPAP/Prereqs/Discrete/Convolution/Order.lean

@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Algebra.Star.Order
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Prereqs.Discrete.Convolution.Basic
 

LeanAPAP/Prereqs/Discrete/LpNorm/Basic.lean

@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Algebra.BigOperators.Order
 import LeanAPAP.Mathlib.Algebra.Order.Group.Abs
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -1,6 +1,5 @@
 import Mathlib.Analysis.MeanInequalitiesPow
 import LeanAPAP.Mathlib.Algebra.BigOperators.Basic
-import LeanAPAP.Mathlib.Algebra.BigOperators.Order
 import LeanAPAP.Mathlib.Algebra.BigOperators.Pi
 import LeanAPAP.Prereqs.Multinomial
 

LeanAPAP/Prereqs/NNRat/Cast/CharZero.lean

@@ -1,5 +1,4 @@
 import Mathlib.Data.Int.CharZero
-import LeanAPAP.Mathlib.Data.Rat.Order
 import LeanAPAP.Mathlib.Data.NNRat.Defs
 import LeanAPAP.Prereqs.NNRat.Cast.Defs
 

LeanAPAP/Prereqs/NNRat/Order.lean

@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Order.Module.Defs
-import LeanAPAP.Prereqs.NNRat.Algebra
+import Mathlib.Tactic.Positivity.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Field.Basic
+import LeanAPAP.Prereqs.NNRat.Algebra
 
 namespace NNRat
 

LeanAPAP/Prereqs/Translate.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Pi
+import Mathlib.Algebra.Star.Order
 import Mathlib.Data.ZMod.Basic
-import LeanAPAP.Mathlib.Algebra.Star.Order
 
 /-!
 # Precomposition operators

lake-manifest.json

@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "8b2dfa4e358ef9969cc5f519810315b205710e24",
+   "rev": "72c702f69ce58dfc92f44b2713ccdc103405cedc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,