Bump mathlib

YaelDillies · Jan 21, 2025 · bcfbd45 · bcfbd45
1 parent af6c796
commit bcfbd45
Show file tree

Hide file tree

Showing 12 changed files with 5 additions and 136 deletions.
diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
@@ -30,7 +30,6 @@ import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
-import LeanCamCombi.Mathlib.Algebra.Ring.Hom.Defs
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
@@ -54,16 +53,12 @@ import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeas
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
 import LeanCamCombi.Mathlib.MeasureTheory.Function.L1Space
-import LeanCamCombi.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Haar.NormedSpace
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
-import LeanCamCombi.Mathlib.Order.BooleanSubalgebra
 import LeanCamCombi.Mathlib.Order.Flag
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
-import LeanCamCombi.Mathlib.Probability.Variance
-import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology
 import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
 import LeanCamCombi.MetricBetween

diff --git a/LeanCamCombi/GrowthInGroups/Chevalley.lean b/LeanCamCombi/GrowthInGroups/Chevalley.lean
@@ -2,7 +2,6 @@ import Mathlib.Data.DFinsupp.WellFounded
 import Mathlib.RingTheory.Localization.Algebra
 import Mathlib.RingTheory.Spectrum.Prime.Polynomial
 import LeanCamCombi.Mathlib.Data.Prod.Lex
-import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum
 
 open Polynomial PrimeSpectrum TensorProduct Topology

diff --git a/LeanCamCombi/GrowthInGroups/Constructible.lean b/LeanCamCombi/GrowthInGroups/Constructible.lean
@@ -3,8 +3,8 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Order.BooleanSubalgebra
 import Mathlib.Topology.Spectral.Hom
-import LeanCamCombi.Mathlib.Order.BooleanSubalgebra
 
 /-!
 # Constructible sets
@@ -342,7 +342,7 @@ lemma IsConstructible.induction_of_isTopologicalBasis {ι : Type*} [Nonempty ι]
         basis.isConstructible' compact_inter _))
     (union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) (hs.union ht))
     (s : Set X) (hs : IsConstructible s) : P s hs := by
-  induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction' with
+  induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction with
   | isSublattice =>
     exact ⟨fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩,
       fun s hs t ht ↦ ⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩⟩

diff --git a/LeanCamCombi/Mathlib/Algebra/Ring/Hom/Defs.lean b/LeanCamCombi/Mathlib/Algebra/Ring/Hom/Defs.lean
diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean b/LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
-import LeanCamCombi.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 
 /-!
 # TODO

diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanCamCombi/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
diff --git a/LeanCamCombi/Mathlib/Order/BooleanSubalgebra.lean b/LeanCamCombi/Mathlib/Order/BooleanSubalgebra.lean
diff --git a/LeanCamCombi/Mathlib/Probability/Variance.lean b/LeanCamCombi/Mathlib/Probability/Variance.lean
diff --git a/LeanCamCombi/Mathlib/RingTheory/FinitePresentation.lean b/LeanCamCombi/Mathlib/RingTheory/FinitePresentation.lean
diff --git a/LeanCamCombi/PhD/VCDim/CondVar.lean b/LeanCamCombi/PhD/VCDim/CondVar.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.MeasureTheory.Integral.Average
+import Mathlib.Probability.Variance
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
 import LeanCamCombi.Mathlib.MeasureTheory.Function.L1Space
-import LeanCamCombi.Mathlib.Probability.Variance
 
 /-!
 # Conditional variance

diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3c2c5041203a2782a0772001c640ecccfe364a5a",
+   "rev": "e3ce54eedb2ab716b7f62aecc31b0308cb7719b8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3c2c5041203a2782a0772001c640ecccfe364a5a",
+   "rev": "e3ce54eedb2ab716b7f62aecc31b0308cb7719b8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,