Documentation
FormalConjecturesForMathlib
Search
return to top
source
Imports
Init
FormalConjecturesForMathlib.AlgebraicGeometry.ProjectiveSpace
FormalConjecturesForMathlib.AlgebraicGeometry.VectorBundle
FormalConjecturesForMathlib.Analysis.HasGaps
FormalConjecturesForMathlib.Combinatorics.Basic
FormalConjecturesForMathlib.Combinatorics.Ramsey
FormalConjecturesForMathlib.Computability.Encoding
FormalConjecturesForMathlib.Geometry.«2d»
FormalConjecturesForMathlib.Geometry.«3d»
FormalConjecturesForMathlib.Geometry.Euclidean
FormalConjecturesForMathlib.Geometry.Metric
FormalConjecturesForMathlib.LinearAlgebra.GeneralLinearGroup
FormalConjecturesForMathlib.LinearAlgebra.SpecialLinearGroup
FormalConjecturesForMathlib.NumberTheory.AdditivelyComplete
FormalConjecturesForMathlib.NumberTheory.CoveringSystem
FormalConjecturesForMathlib.NumberTheory.Lacunary
FormalConjecturesForMathlib.NumberTheory.PrimeGap
FormalConjecturesForMathlib.NumberTheory.WallSunSunPrimes
FormalConjecturesForMathlib.Algebra.GCDMonoid.Finset
FormalConjecturesForMathlib.Algebra.Group.Indicator
FormalConjecturesForMathlib.Algebra.Polynomial.Algebra
FormalConjecturesForMathlib.Algebra.Polynomial.Basic
FormalConjecturesForMathlib.Algebra.Polynomial.HasseDeriv
FormalConjecturesForMathlib.Analysis.Asymptotics.Basic
FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
FormalConjecturesForMathlib.Combinatorics.AP.Basic
FormalConjecturesForMathlib.Combinatorics.Additive.Basis
FormalConjecturesForMathlib.Combinatorics.Additive.Convolution
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Balanced
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Coloring
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.DiamExtra
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers
FormalConjecturesForMathlib.Computability.TuringMachine.Notation
FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine
FormalConjecturesForMathlib.Data.Finset.Empty
FormalConjecturesForMathlib.Data.Finset.OrdConnected
FormalConjecturesForMathlib.Data.Nat.Full
FormalConjecturesForMathlib.Data.Nat.Init
FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac
FormalConjecturesForMathlib.Data.Nat.Squarefree
FormalConjecturesForMathlib.Data.Real.Cardinality
FormalConjecturesForMathlib.Data.Real.Constants
FormalConjecturesForMathlib.Data.Set.Bdd
FormalConjecturesForMathlib.Data.Set.Density
FormalConjecturesForMathlib.Data.Set.Triplewise
FormalConjecturesForMathlib.Data.ZMod.PerfectDifferenceSet
FormalConjecturesForMathlib.NumberTheory.DirichletCharacter.Basic
FormalConjecturesForMathlib.NumberTheory.LegendreSymbol.Basic
FormalConjecturesForMathlib.Order.Filter.Cofinite
FormalConjecturesForMathlib.SetTheory.Cardinal.Arithmetic
FormalConjecturesForMathlib.SetTheory.Cardinal.Continuum
FormalConjecturesForMathlib.SetTheory.Cardinal.SimpleGraph
FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Definitions
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Domination
FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Invariants
FormalConjecturesForMathlib.Data.Nat.Factorization.Basic
FormalConjecturesForMathlib.Data.Nat.Prime.Composite
FormalConjecturesForMathlib.Data.Nat.Prime.Defs
FormalConjecturesForMathlib.Data.Nat.Prime.Finset
FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate
FormalConjecturesForMathlib.Order.Filter.atTopBot.Finset
FormalConjecturesForMathlib.Order.Interval.Finset.Basic
FormalConjecturesForMathlib.Order.Interval.Finset.Nat
FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Group
FormalConjecturesForMathlib.Topology.Algebra.InfiniteSum.Order
FormalConjecturesForMathlib.Algebra.Order.Group.Pointwise.Interval
FormalConjecturesForMathlib.Algebra.Group.Action.Pointwise.Set.Basic
Imported by