Skip to content

Commit

Permalink
Bump mathlib
Browse files Browse the repository at this point in the history
  • Loading branch information
@YaelDillies
YaelDillies committed Jan 24, 2025
1 parent f720b12 commit 779ca91
Show file tree
Hide file tree
Showing 25 changed files with 167 additions and 1,527 deletions.
11 changes: 1 addition & 10 deletions LeanCamCombi.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,7 @@ import LeanCamCombi.ExtrProbCombi.Containment
import LeanCamCombi.ExtrProbCombi.GiantComponent
import LeanCamCombi.GraphTheory.ExampleSheet1
import LeanCamCombi.GraphTheory.ExampleSheet2
import LeanCamCombi.GroupMarking
import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
import LeanCamCombi.GrowthInGroups.Chevalley
import LeanCamCombi.GrowthInGroups.ChevalleyComplex
import LeanCamCombi.GrowthInGroups.Constructible
import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum
import LeanCamCombi.GrowthInGroups.ConstructibleSetData
import LeanCamCombi.GrowthInGroups.Lecture1
import LeanCamCombi.GrowthInGroups.Lecture2
import LeanCamCombi.GrowthInGroups.Lecture3
Expand All @@ -25,13 +19,12 @@ import LeanCamCombi.Impact
import LeanCamCombi.Kneser.Kneser
import LeanCamCombi.Kneser.KneserRuzsa
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.Analysis.Convex.Exposed
import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
import LeanCamCombi.Mathlib.Analysis.Convex.Independence
import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
Expand All @@ -41,7 +34,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
import LeanCamCombi.Mathlib.Data.List.DropRight
import LeanCamCombi.Mathlib.Data.Multiset.Basic
import LeanCamCombi.Mathlib.Data.Set.Image
import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Expand All @@ -51,7 +43,6 @@ 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.RingTheory.Spectrum.Prime.Topology
import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
import LeanCamCombi.MetricBetween
import LeanCamCombi.MinkowskiCaratheodory
Expand Down
273 changes: 0 additions & 273 deletions LeanCamCombi/GroupMarking.lean
View file

This file was deleted.

Loading

0 comments on commit 779ca91

Please sign in to comment.