Skip to content

Commit a71c6fe

Browse files
committed
Bump mathlib
1 parent f720b12 commit a71c6fe

File tree

24 files changed

+167
-1514
lines changed

24 files changed

+167
-1514
lines changed

LeanCamCombi.lean

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,7 @@ import LeanCamCombi.ExtrProbCombi.Containment
1010
import LeanCamCombi.ExtrProbCombi.GiantComponent
1111
import LeanCamCombi.GraphTheory.ExampleSheet1
1212
import LeanCamCombi.GraphTheory.ExampleSheet2
13-
import LeanCamCombi.GroupMarking
14-
import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
15-
import LeanCamCombi.GrowthInGroups.Chevalley
1613
import LeanCamCombi.GrowthInGroups.ChevalleyComplex
17-
import LeanCamCombi.GrowthInGroups.Constructible
18-
import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum
19-
import LeanCamCombi.GrowthInGroups.ConstructibleSetData
2014
import LeanCamCombi.GrowthInGroups.Lecture1
2115
import LeanCamCombi.GrowthInGroups.Lecture2
2216
import LeanCamCombi.GrowthInGroups.Lecture3
@@ -25,13 +19,12 @@ import LeanCamCombi.Impact
2519
import LeanCamCombi.Kneser.Kneser
2620
import LeanCamCombi.Kneser.KneserRuzsa
2721
import LeanCamCombi.Kneser.MulStab
28-
import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
2922
import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
30-
import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
3123
import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
3224
import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
3325
import LeanCamCombi.Mathlib.Analysis.Convex.Independence
3426
import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
27+
import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
3528
import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
3629
import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
3730
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
@@ -41,7 +34,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
4134
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
4235
import LeanCamCombi.Mathlib.Data.List.DropRight
4336
import LeanCamCombi.Mathlib.Data.Multiset.Basic
44-
import LeanCamCombi.Mathlib.Data.Set.Image
4537
import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
4638
import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
4739
import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
@@ -51,7 +43,6 @@ import LeanCamCombi.Mathlib.Order.Flag
5143
import LeanCamCombi.Mathlib.Order.Partition.Finpartition
5244
import LeanCamCombi.Mathlib.Order.RelIso.Group
5345
import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
54-
import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology
5546
import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
5647
import LeanCamCombi.MetricBetween
5748
import LeanCamCombi.MinkowskiCaratheodory

LeanCamCombi/GroupMarking.lean

Lines changed: 0 additions & 273 deletions
This file was deleted.

0 commit comments

Comments
 (0)