`FormalConjecturesForMathlib.lean`

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

This file declares nothing itself. It gathers the 221 imports below, so a file that imports it gets all of them.

Imports

FormalConjecturesForMathlib.Algebra.GCDMonoid.Finset
FormalConjecturesForMathlib.Algebra.GradedMonoid
FormalConjecturesForMathlib.Algebra.Group.Action.Pointwise.Set.Basic
FormalConjecturesForMathlib.Algebra.Group.GrowthFunction
FormalConjecturesForMathlib.Algebra.Group.Indicator
FormalConjecturesForMathlib.Algebra.Homology.DerivedCategory.Ext.GradedAlgebra
FormalConjecturesForMathlib.Algebra.MvPolynomial.PoissonBracket
FormalConjecturesForMathlib.Algebra.MvPolynomial.RegularFunction
FormalConjecturesForMathlib.Algebra.Order.Group.Pointwise.Interval
FormalConjecturesForMathlib.Algebra.Polynomial.Algebra
FormalConjecturesForMathlib.Algebra.Polynomial.Basic
FormalConjecturesForMathlib.Algebra.Polynomial.HasseDeriv
FormalConjecturesForMathlib.Algebra.Powerfree
FormalConjecturesForMathlib.Algebra.QuadraticAlgebra.Instances
FormalConjecturesForMathlib.Algebra.Ring.PythagorasNumber
FormalConjecturesForMathlib.AlgebraicGeometry.EllipticCurve.GlobalPeriod
FormalConjecturesForMathlib.AlgebraicGeometry.EllipticCurve.MinimalDiscriminant
FormalConjecturesForMathlib.AlgebraicGeometry.EllipticCurve.Regulator
FormalConjecturesForMathlib.AlgebraicGeometry.EllipticCurve.Tamagawa
FormalConjecturesForMathlib.AlgebraicGeometry.EllipticCurve.TateShafarevich
FormalConjecturesForMathlib.AlgebraicGeometry.ProjectiveSpace
FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
FormalConjecturesForMathlib.Analysis.HasGaps
FormalConjecturesForMathlib.Analysis.Matrix.Spectrum
FormalConjecturesForMathlib.Analysis.Real.Cardinality
FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter
FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
FormalConjecturesForMathlib.Combinatorics.AP.Basic
FormalConjecturesForMathlib.Combinatorics.Additive.Basis
FormalConjecturesForMathlib.Combinatorics.Additive.Convolution
FormalConjecturesForMathlib.Combinatorics.Additive.Coset
FormalConjecturesForMathlib.Combinatorics.Additive.DifferenceBasis
FormalConjecturesForMathlib.Combinatorics.Additive.RestrictedSumset
FormalConjecturesForMathlib.Combinatorics.Additive.VCDim
FormalConjecturesForMathlib.Combinatorics.Basic
FormalConjecturesForMathlib.Combinatorics.Digraph.Tournament
FormalConjecturesForMathlib.Combinatorics.Hypergraph.Basic
FormalConjecturesForMathlib.Combinatorics.Hypergraph.Extremal
FormalConjecturesForMathlib.Combinatorics.Hypergraph.Finite
FormalConjecturesForMathlib.Combinatorics.Hypergraph.Uniform
FormalConjecturesForMathlib.Combinatorics.LatinSquare
FormalConjecturesForMathlib.Combinatorics.LimitObjects.Graphon
FormalConjecturesForMathlib.Combinatorics.LimitObjects.Tournamenton
FormalConjecturesForMathlib.Combinatorics.Ramsey
FormalConjecturesForMathlib.Combinatorics.Ramsey.Diagonal
FormalConjecturesForMathlib.Combinatorics.SetFamily.PropertyB
FormalConjecturesForMathlib.Combinatorics.SetFamily.Sunflower
FormalConjecturesForMathlib.Combinatorics.SetFamily.UnionFree
FormalConjecturesForMathlib.Combinatorics.SetFamily.VCDim
FormalConjecturesForMathlib.Combinatorics.SetTheory.PartitionRelation
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationNumber
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Chordal
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Circumference
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Clique
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Coloring.Vertex
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CompleteGraphEdgeCount
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Cvetkovic
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Cycle
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.CycleRank
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Decomposition
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degeneracy
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Domination
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Eccentricity
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.EdgeColouring
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.FractionalAlpha
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HarmonicIndex
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Hypercube
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Independence
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Induced
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.InducedTreeNeighborhood
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Johnson
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.LargestInducedTree
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.LovaszTheta
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Matching
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.PathCover
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Prod
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.QuasiLineGraph
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Ramsey
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Residue
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Saturation
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SpanningTree
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SubgraphIsomorphism
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SzegedIndex
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Temperature
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WellTotallyDominated
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.WienerIndex
FormalConjecturesForMathlib.Combinatorics.YoungDiagram
FormalConjecturesForMathlib.Computability.AutomaticSequence
FormalConjecturesForMathlib.Computability.BitstringEncoding
FormalConjecturesForMathlib.Computability.Complexity
FormalConjecturesForMathlib.Computability.DFA
FormalConjecturesForMathlib.Computability.Primrec
FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers
FormalConjecturesForMathlib.Computability.TuringMachine.Notation
FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine
FormalConjecturesForMathlib.Data.Bool.Basic
FormalConjecturesForMathlib.Data.Finset.Card
FormalConjecturesForMathlib.Data.Finset.Powerset
FormalConjecturesForMathlib.Data.Finset.ReciprocalSum
FormalConjecturesForMathlib.Data.Int.IntermediateValue
FormalConjecturesForMathlib.Data.Int.Order.Basic
FormalConjecturesForMathlib.Data.Nat.Factorization.Basic
FormalConjecturesForMathlib.Data.Nat.Full
FormalConjecturesForMathlib.Data.Nat.Init
FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac
FormalConjecturesForMathlib.Data.Nat.PerfectPower
FormalConjecturesForMathlib.Data.Nat.Prime.Composite
FormalConjecturesForMathlib.Data.Nat.Prime.Defs
FormalConjecturesForMathlib.Data.Nat.Prime.Finset
FormalConjecturesForMathlib.Data.Nat.Prime.Infinite
FormalConjecturesForMathlib.Data.Nat.Squarefree
FormalConjecturesForMathlib.Data.Real.Constants
FormalConjecturesForMathlib.Data.Real.NearestInt
FormalConjecturesForMathlib.Data.Set.Density
FormalConjecturesForMathlib.Data.Set.Interval
FormalConjecturesForMathlib.Data.Set.Triplewise
FormalConjecturesForMathlib.Data.Sym.Sym2
FormalConjecturesForMathlib.Data.ZMod.Fp
FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet
FormalConjecturesForMathlib.Dynamics.SymbolicDynamics.BlockComplexity
FormalConjecturesForMathlib.FieldTheory.AbsoluteGaloisGroup
FormalConjecturesForMathlib.FieldTheory.MilnorKTheory
FormalConjecturesForMathlib.FieldTheory.MvRatFunc.Defs
FormalConjecturesForMathlib.Geometry.Euclidean
FormalConjecturesForMathlib.Geometry.Group.Hyperbolic
FormalConjecturesForMathlib.Geometry.Group.WordMetric
FormalConjecturesForMathlib.Geometry.Group.WordProd
FormalConjecturesForMathlib.Geometry.Manifold.LieGroupPresentation
FormalConjecturesForMathlib.Geometry.Metric
FormalConjecturesForMathlib.Geometry.«2d»
FormalConjecturesForMathlib.Geometry.«3d»
FormalConjecturesForMathlib.GroupTheory.Torsion
FormalConjecturesForMathlib.Lean.Elab.InfoTree.Util
FormalConjecturesForMathlib.LinearAlgebra.AffineSpace.Simplex.Basic
FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup
FormalConjecturesForMathlib.LinearAlgebra.QuadraticForm.UInvariant
FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup
FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate
FormalConjecturesForMathlib.ModelTheory.Decidability
FormalConjecturesForMathlib.ModelTheory.Encoding
FormalConjecturesForMathlib.ModelTheory.Real
FormalConjecturesForMathlib.NumberTheory.AdditionChain
FormalConjecturesForMathlib.NumberTheory.AdditiveComplement
FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete
FormalConjecturesForMathlib.NumberTheory.AlmostPrime
FormalConjecturesForMathlib.NumberTheory.Amicable
FormalConjecturesForMathlib.NumberTheory.AutomaticNumber
FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet
FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.CenterAction
FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.LieDeriv
FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.Subgroups
FormalConjecturesForMathlib.NumberTheory.BeurlingPrimes
FormalConjecturesForMathlib.NumberTheory.Carmichael
FormalConjecturesForMathlib.NumberTheory.CoveringSystem
FormalConjecturesForMathlib.NumberTheory.DiophantineApproximation.ZNumber
FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic
FormalConjecturesForMathlib.NumberTheory.Divisors
FormalConjecturesForMathlib.NumberTheory.ExpansionEntropy
FormalConjecturesForMathlib.NumberTheory.Harmonic
FormalConjecturesForMathlib.NumberTheory.Lacunary
FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic
FormalConjecturesForMathlib.NumberTheory.MultiplicativelyIndependent
FormalConjecturesForMathlib.NumberTheory.NormalNumber
FormalConjecturesForMathlib.NumberTheory.NumberField.FundamentalDiscriminant
FormalConjecturesForMathlib.NumberTheory.NumberField.Quadratic
FormalConjecturesForMathlib.NumberTheory.PisotNumber
FormalConjecturesForMathlib.NumberTheory.PracticalNumbers
FormalConjecturesForMathlib.NumberTheory.PrimeGap
FormalConjecturesForMathlib.NumberTheory.Primitive
FormalConjecturesForMathlib.NumberTheory.SierpinskiNumber
FormalConjecturesForMathlib.NumberTheory.SmoothScale
FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes
FormalConjecturesForMathlib.NumberTheory.WieferichPrime
FormalConjecturesForMathlib.Order.Bounds.Basic
FormalConjecturesForMathlib.Order.Filter.Cofinite
FormalConjecturesForMathlib.Order.Filter.atTopBot.Finset
FormalConjecturesForMathlib.Order.Interval.Finset.Basic
FormalConjecturesForMathlib.Order.Interval.Finset.Nat
FormalConjecturesForMathlib.Order.Nat
FormalConjecturesForMathlib.Order.Unimodular
FormalConjecturesForMathlib.Probability.FiniteMethod
FormalConjecturesForMathlib.RepresentationTheory.Homological.ContCohomology.Sha
FormalConjecturesForMathlib.RingTheory.Bialgebra.Cohomology
FormalConjecturesForMathlib.RingTheory.Bialgebra.TrivialModule
FormalConjecturesForMathlib.RingTheory.CohenMacaulayModule
FormalConjecturesForMathlib.RingTheory.Ideal.Basic
FormalConjecturesForMathlib.RingTheory.Ideal.Defs
FormalConjecturesForMathlib.RingTheory.Ideal.Maximal
FormalConjecturesForMathlib.RingTheory.IntersectionMultiplicity
FormalConjecturesForMathlib.RingTheory.MvPolynomial.LexPlusPowers
FormalConjecturesForMathlib.RingTheory.Noetherian.Defs
FormalConjecturesForMathlib.RingTheory.SystemOfParameters
FormalConjecturesForMathlib.RingTheory.Valuation.LocalUniformization
FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic
FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum
FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph
FormalConjecturesForMathlib.Tactic.Linter.Term
FormalConjecturesForMathlib.Topology.AbsoluteNeighborhoodRetract
FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Group
FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Order
FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Real
FormalConjecturesForMathlib.Topology.CardinalInvariants
FormalConjecturesForMathlib.Topology.Discrete
FormalConjecturesForMathlib.Topology.GDelta
FormalConjecturesForMathlib.Topology.Homogeneous
FormalConjecturesForMathlib.Topology.LebesgueCoveringDimension
FormalConjecturesForMathlib.Topology.MetricSpace.GromovProduct
FormalConjecturesForMathlib.Topology.MetricSpace.Hyperbolic
FormalConjecturesForMathlib.Topology.MetricSpace.MetricSeparated

Imported by 1 file

FormalConjecturesUtil.lean