-
Notifications
You must be signed in to change notification settings - Fork 8
/
LeanCamCombi.lean
63 lines (63 loc) · 3.01 KB
/
LeanCamCombi.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
import LeanCamCombi.Archive.CauchyDavenportFromKneser
import LeanCamCombi.BernoulliSeq
import LeanCamCombi.ConvexityRefactor.Defs
import LeanCamCombi.ConvexityRefactor.StdSimplex
import LeanCamCombi.Corners.CombiDegen
import LeanCamCombi.DiscreteDeriv
import LeanCamCombi.ErdosRenyi.Basic
import LeanCamCombi.ErdosRenyi.BollobasContainment
import LeanCamCombi.ErdosRenyi.Connectivity
import LeanCamCombi.ErdosRenyi.GiantComponent
import LeanCamCombi.ExampleSheets.Graph.ES1
import LeanCamCombi.ExampleSheets.Graph.ES2
import LeanCamCombi.GrowthInGroups.Lecture1
import LeanCamCombi.GrowthInGroups.Lecture2
import LeanCamCombi.GrowthInGroups.SmallTripling
import LeanCamCombi.Impact
import LeanCamCombi.Incidence
import LeanCamCombi.Kneser.Kneser
import LeanCamCombi.Kneser.KneserRuzsa
import LeanCamCombi.Kneser.MulStab
import LeanCamCombi.LittlewoodOfford
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
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.PluenneckeRuzsa
import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Degree
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
import LeanCamCombi.Mathlib.Data.List.DropRight
import LeanCamCombi.Mathlib.Data.Multiset.Basic
import LeanCamCombi.Mathlib.Data.Set.Pointwise.Finite
import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
import LeanCamCombi.Mathlib.GroupTheory.Coset.Card
import LeanCamCombi.Mathlib.GroupTheory.Nilpotent
import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup.Finite
import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
import LeanCamCombi.Mathlib.Order.Interval.Finset.Defs
import LeanCamCombi.Mathlib.Order.Partition.Finpartition
import LeanCamCombi.Mathlib.Order.SuccPred.Relation
import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
import LeanCamCombi.MetricBetween
import LeanCamCombi.MinkowskiCaratheodory
import LeanCamCombi.OrderShatter
import LeanCamCombi.PhD.VCDim.Basic
import LeanCamCombi.SimplicialComplex.Basic
import LeanCamCombi.SimplicialComplex.Finite
import LeanCamCombi.SimplicialComplex.Pure
import LeanCamCombi.SimplicialComplex.Simplex
import LeanCamCombi.SimplicialComplex.Skeleton
import LeanCamCombi.SimplicialComplex.Subdivision
import LeanCamCombi.SliceRank
import LeanCamCombi.SylvesterChvatal
import LeanCamCombi.VanDenBergKesten