Repository navigation
Expand file tree
/
Copy pathFormalConjecturesForMathlib.lean
More file actions
153 lines (149 loc) · 10.1 KB
/
Copy pathFormalConjecturesForMathlib.lean
File metadata and controls
153 lines (149 loc) · 10.1 KB
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesForMathlib.Algebra.GCDMonoid.Finset
public import FormalConjecturesForMathlib.Algebra.Group.Action.Pointwise.Set.Basic
public import FormalConjecturesForMathlib.Algebra.Group.GrowthFunction
public import FormalConjecturesForMathlib.Algebra.Group.Indicator
public import FormalConjecturesForMathlib.Algebra.Order.Group.Pointwise.Interval
public import FormalConjecturesForMathlib.Algebra.Polynomial.Algebra
public import FormalConjecturesForMathlib.Algebra.Polynomial.Basic
public import FormalConjecturesForMathlib.Algebra.Polynomial.HasseDeriv
public import FormalConjecturesForMathlib.Algebra.Powerfree
public import FormalConjecturesForMathlib.Algebra.QuadraticAlgebra.Basic
public import FormalConjecturesForMathlib.Algebra.QuadraticAlgebra.Instances
public import FormalConjecturesForMathlib.AlgebraicGeometry.ProjectiveSpace
public import FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
public import FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
public import FormalConjecturesForMathlib.Analysis.HasGaps
public import FormalConjecturesForMathlib.Analysis.Real.Cardinality
public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
public import FormalConjecturesForMathlib.Combinatorics.AP.Basic
public import FormalConjecturesForMathlib.Combinatorics.Additive.Basis
public import FormalConjecturesForMathlib.Combinatorics.Additive.Convolution
public import FormalConjecturesForMathlib.Combinatorics.Additive.Coset
public import FormalConjecturesForMathlib.Combinatorics.Additive.DifferenceBasis
public import FormalConjecturesForMathlib.Combinatorics.Additive.RestrictedSumset
public import FormalConjecturesForMathlib.Combinatorics.Additive.VCDim
public import FormalConjecturesForMathlib.Combinatorics.Basic
public import FormalConjecturesForMathlib.Combinatorics.Hypergraph.ThreeUniform
public import FormalConjecturesForMathlib.Combinatorics.LatinSquare
public import FormalConjecturesForMathlib.Combinatorics.Ramsey
public import FormalConjecturesForMathlib.Combinatorics.Ramsey.Diagonal
public import FormalConjecturesForMathlib.Combinatorics.SetFamily.Sunflower
public import FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim
public import FormalConjecturesForMathlib.Combinatorics.SetTheory.PartitionRelation
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Circumference
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Clique
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Coloring
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CompleteGraphEdgeCount
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CycleRank
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SzegedIndex
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.FractionalAlpha
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.LovaszTheta
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WienerIndex
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Cvetkovic
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Temperature
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Eccentricity
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.PathCover
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.EdgeColouring
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.LargestInducedTree
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WellTotallyDominated
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Johnson
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Ramsey
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Matching
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SpanningTree
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph
public import FormalConjecturesForMathlib.Combinatorics.YoungDiagram
public import FormalConjecturesForMathlib.Computability.DFA
public import FormalConjecturesForMathlib.Computability.Encoding
public import FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers
public import FormalConjecturesForMathlib.Computability.TuringMachine.Notation
public import FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine
public import FormalConjecturesForMathlib.Data.Finset.Card
public import FormalConjecturesForMathlib.Data.Finset.Powerset
public import FormalConjecturesForMathlib.Data.Finset.ReciprocalSum
public import FormalConjecturesForMathlib.Data.Int.IntermediateValue
public import FormalConjecturesForMathlib.Data.Nat.Factorization.Basic
public import FormalConjecturesForMathlib.Data.Nat.Full
public import FormalConjecturesForMathlib.Data.Nat.Init
public import FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac
public import FormalConjecturesForMathlib.Data.Nat.PerfectPower
public import FormalConjecturesForMathlib.Data.Nat.Prime.Composite
public import FormalConjecturesForMathlib.Data.Nat.Prime.Defs
public import FormalConjecturesForMathlib.Data.Nat.Prime.Finset
public import FormalConjecturesForMathlib.Data.Nat.Squarefree
public import FormalConjecturesForMathlib.Data.Real.Constants
public import FormalConjecturesForMathlib.Data.Real.NearestInt
public import FormalConjecturesForMathlib.Data.Set.Density
public import FormalConjecturesForMathlib.Data.Set.Interval
public import FormalConjecturesForMathlib.Data.Set.Triplewise
public import FormalConjecturesForMathlib.Data.ZMod.Fp
public import FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet
public import FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs
public import FormalConjecturesForMathlib.Geometry.Euclidean
public import FormalConjecturesForMathlib.Geometry.Metric
public import FormalConjecturesForMathlib.Geometry.«2d»
public import FormalConjecturesForMathlib.Geometry.«3d»
public import FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic
public import FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup
public import FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup
public import FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate
public import FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete
public import FormalConjecturesForMathlib.NumberTheory.Amicable
public import FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes
public import FormalConjecturesForMathlib.NumberTheory.Carmichael
public import FormalConjecturesForMathlib.NumberTheory.CoveringSystem
public import FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic
public import FormalConjecturesForMathlib.NumberTheory.Divisors
public import FormalConjecturesForMathlib.NumberTheory.Lacunary
public import FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic
public import FormalConjecturesForMathlib.NumberTheory.NormalNumber
public import FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic
public import FormalConjecturesForMathlib.NumberTheory.PisotNumber
public import FormalConjecturesForMathlib.NumberTheory.PracticalNumbers
public import FormalConjecturesForMathlib.NumberTheory.PrimeGap
public import FormalConjecturesForMathlib.NumberTheory.Primitive
public import FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber
public import FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes
public import FormalConjecturesForMathlib.Order.Filter.Cofinite
public import FormalConjecturesForMathlib.Order.Filter.atTopBot.Finset
public import FormalConjecturesForMathlib.Order.Interval.Finset.Basic
public import FormalConjecturesForMathlib.Order.Interval.Finset.Nat
public import FormalConjecturesForMathlib.Probability.FiniteMethod
public import FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic
public import FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum
public import FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph
public import FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract
public import FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Group
public import FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Order
public import FormalConjecturesForMathlib.Topology.Discrete
public import FormalConjecturesForMathlib.Topology.GDelta
public import FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension
public import FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated
public import FormalConjecturesForMathlib.Topology.Homogeneous