-
Notifications
You must be signed in to change notification settings - Fork 257
Expand file tree
/
Copy pathFormalConjecturesForMathlib.lean
More file actions
103 lines (99 loc) · 6.46 KB
/
FormalConjecturesForMathlib.lean
File metadata and controls
103 lines (99 loc) · 6.46 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
/-
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.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.AlgebraicGeometry.ProjectiveSpace
public import FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
public import FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
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.VCDim
public import FormalConjecturesForMathlib.Combinatorics.Basic
public import FormalConjecturesForMathlib.Combinatorics.LatinSquare
public import FormalConjecturesForMathlib.Combinatorics.Ramsey
public import FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Clique
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Coloring
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Domination
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Invariants
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Johnson
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
public import FormalConjecturesForMathlib.Combinatorics.YoungDiagram
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.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.PerfectDifferenceSet
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.CoveringSystem
public import FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic
public import FormalConjecturesForMathlib.NumberTheory.Lacunary
public import FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic
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.SetTheory.Cardinal.Arithmetic
public import FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum
public import FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph
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.MetricSpace.MetricSeparated