General documentation

index
foundational types

Library

Aesop (file)
Builder (file)
Apply
Basic
Cases
Constructors
Default
Forward
NormSimp
Tactic
Unfold
BuiltinRules (file)
ApplyHyps
Assumption
DestructProducts
Ext
Intros
Split
Subst
Frontend (file)
Extension (file)
Init
Attribute
Basic
Command
ElabM
RuleExpr
Tactic
Index (file)
Basic
Options (file)
Internal
Public
Rule (file)
Basic
Name
RuleTac (file)
Apply
Basic
Cases
Forward
Preprocess
Tactic
Search
Expansion (file)
Basic
Norm
Simp
Queue (file)
Class
ExpandSafePrefix
Main
RuleSelection
SearchM
Tree (file)
AddRapp
Check
Data
ExtractProof
ExtractScript
Free
RunMetaM
State
Tracing
Traversal
TreeM
UnsafeQueue
Util
Basic
EqualUpToIds
Tactic
UnionFind
UnorderedArraySet
Check
Constants
Main
Nanos
Percent
Profiling
RuleSet
Script
Tracing
Archive (file)
Examples
IfNormalization
Result
Statement
WithoutAesop
MersennePrimes
PropEncodable
Imo
Imo1959Q1
Imo1960Q1
Imo1962Q1
Imo1962Q4
Imo1964Q1
Imo1969Q1
Imo1972Q5
Imo1975Q1
Imo1977Q6
Imo1981Q3
Imo1987Q1
Imo1988Q6
Imo1994Q1
Imo1998Q2
Imo2001Q2
Imo2001Q6
Imo2005Q3
Imo2005Q4
Imo2006Q3
Imo2006Q5
Imo2008Q2
Imo2008Q3
Imo2008Q4
Imo2011Q3
Imo2011Q5
Imo2013Q1
Imo2013Q5
Imo2019Q1
Imo2019Q2
Imo2019Q4
Imo2020Q2
Imo2021Q1
MiuLanguage
Basic
DecisionNec
DecisionSuf
OxfordInvariants
Summer2021
Week3P1
Wiedijk100Theorems
AbelRuffini
AreaOfACircle
AscendingDescendingSequences
BallotProblem
BirthdayProblem
CubingACube
FriendshipGraphs
HeronsFormula
InverseTriangleSum
Konigsberg
Partition
PerfectNumbers
SolutionOfCubic
SumOfPrimeReciprocalsDiverges
Arithcc
Sensitivity
ZagierTwoSquares
Counterexamples (file)
CanonicallyOrderedCommSemiringTwoMul
CharPZeroNeCharZero
CliffordAlgebra_not_injective
Cyclotomic105
DirectSumIsInternal
Girard
HomogeneousPrimeNotPrime
LinearOrderWithPosMulPosEqZero
MapFloor
Monic_nonRegular
Phillips
Pseudoelement
QuadraticForm
SeminormLatticeNotDistrib
SorgenfreyLine
ZeroDivisorsInAddMonoidAlgebras
Init (file)
Control (file)
Basic
EState
Except
ExceptCps
Id
Lawful
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Basic
BasicAux
BinSearch
DecidableEq
InsertionSort
Mem
QSort
Subarray
ByteArray (file)
Basic
Char (file)
Basic
Fin (file)
Basic
Log2
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Int (file)
Basic
List (file)
Basic
BasicAux
Control
Nat (file)
Basic
Bitwise
Control
Div
Gcd
Linear
Log2
Power2
SOM
Option (file)
Basic
BasicAux
Instances
String (file)
Basic
Extra
ToString (file)
Basic
Macro
UInt (file)
Basic
Log2
AC
Basic
Channel
Float
Hashable
OfScientific
Ord
Prod
Queue
Random
Range
Repr
Stream
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
Classical
Coe
Conv
Core
Dynamic
Hints
Meta
MetaTypes
Notation
NotationExtra
Prelude
ShareCommon
SimpLemmas
SizeOf
SizeOfLemmas
Tactics
Util
WF
WFTactics
Lake (file)
Build (file)
Actions
Common
Context
Data
Executable
Facets
Imports
Index
Info
Job
Key
Library
Module
Monad
Package
Store
Targets
Topological
Trace
CLI
Actions
Config (file)
Context
Dependency
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InstallPath
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Module
Monad
Opaque
Package
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
Config
DeclUtil
Extensions
Meta
Package
Require
Script
Targets
Load
Config
Util
Async
Binder
Casing
Compare
Cycle
DRBMap
EStateT
EquipT
Error
Exit
Family
Git
Lift
List
Log
Name
NativeLib
Opaque
OptionIO
OrdHashSet
OrderedTagAttribute
Platform
Proc
RBArray
Store
StoreInsts
Sugar
Task
Version
Lean (file)
Compiler (file)
IR (file)
Basic
Borrow
Boxing
Checker
CompilerM
CtorLayout
ElimDeadBranches
ElimDeadVars
EmitC
EmitUtil
ExpandResetReuse
Format
FreeVars
LiveVars
NormIds
PushProj
RC
ResetReuse
SimpCase
Sorry
UnboxResult
LCNF (file)
Simp (file)
Basic
Config
ConstantFold
DefaultAlt
DiscrM
FunDeclInfo
InlineCandidate
InlineProj
JpCases
Main
SimpM
SimpValue
Used
AlphaEqv
AuxDeclCache
BaseTypes
Basic
Bind
CSE
Check
Closure
CompatibleTypes
CompilerM
ConfigOptions
DeclHash
DependsOn
ElimDead
ElimDeadBranches
FVarUtil
FixedParams
FloatLetIn
ForEachExpr
InferType
Internalize
JoinPoints
LCtx
LambdaLifting
Level
Main
MonadScope
MonoTypes
OtherDecl
PassManager
Passes
PhaseExt
PrettyPrinter
PullFunDecls
PullLetDecls
ReduceArity
ReduceJpArity
Renaming
ScopeM
SpecInfo
Specialize
Testing
ToDecl
ToExpr
ToLCNF
ToMono
Types
Util
AtMostOnce
BorrowedAnnotation
CSimpAttr
ClosedTermCache
ConstFolding
ExportAttr
ExternAttr
FFI
ImplementedByAttr
InitAttr
InlineAttrs
Main
NameMangling
NeverExtractAttr
NoncomputableAttr
Old
Options
Specialize
Data (file)
Json (file)
Basic
FromToJson
Parser
Printer
Stream
Lsp (file)
Basic
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Workspace
Xml (file)
Basic
Parser
AssocList
Format
FuzzyMatching
HashMap
HashSet
JsonRpc
KVMap
LBool
LOption
Name
NameMap
NameTrie
OpenDecl
Options
Parsec
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RBMap
RBTree
Rat
SMap
SSet
Trie
Elab (file)
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
TypeName
Util
InfoTree (file)
Main
Types
PreDefinition (file)
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndPred
Main
Preprocess
SmartUnfolding
WF (file)
Eqns
Fix
Ite
Main
PackDomain
PackMutual
Rel
TerminationHint
Basic
Eqns
Main
MkInhabitant
Quotation (file)
Precheck
Util
Tactic (file)
Conv (file)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Basic
BuiltinTactic
Cache
Calc
Config
Congr
Delta
ElabTerm
Generalize
Induction
Injection
Location
Match
Meta
Rewrite
Simp
Split
Unfold
App
Arg
Attributes
AutoBound
AuxDef
Binders
BindersUtil
BuiltinCommand
BuiltinNotation
BuiltinTerm
Calc
Command
ComputedFields
Config
DeclModifiers
DeclUtil
Declaration
DeclarationRange
DefView
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
Import
Inductive
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
Mixfix
MutualDef
Notation
Open
ParseImportsFast
PatternVar
Print
RecAppSyntax
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Term
Util
Linter (file)
Basic
Builtin
Deprecated
MissingDocs
UnusedVariables
Util
Meta (file)
Match (file)
Basic
CaseArraySizes
CaseValues
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
Tactic (file)
AC (file)
Main
LinearArith (file)
Nat (file)
Basic
Simp
Solver
Basic
Main
Simp
Solver
Simp (file)
Main
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Types
Acyclic
Apply
Assert
Assumption
AuxLemma
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
FVarSubst
Generalize
Induction
Injection
Intro
Refl
Rename
Replace
Revert
Rewrite
Split
SplitIf
Subst
Unfold
UnifyEq
Util
ACLt
AbstractMVars
AbstractNestedProofs
AppBuilder
Basic
CasesOn
Check
Closure
Coe
CollectFVars
CollectMVars
CongrTheorems
Constructions
DecLevel
DiscrTree
DiscrTreeTypes
Eqns
Eval
ExprDefEq
ExprLens
ExprTraverse
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetUnfoldableConst
GlobalInstances
IndPredBelow
Inductive
InferType
Injective
Instances
KAbstract
KExprMap
LevelDefEq
MatchUtil
Offset
PPGoal
RecursorInfo
Reduce
ReduceEval
SizeOf
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (file)
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
Tactic
Term
Types
ParserCompiler (file)
Attribute
PrettyPrinter (file)
Delaborator (file)
Basic
Builtins
Options
SubExpr
TopDownAnalyze
Basic
Formatter
Parenthesizer
Server (file)
FileWorker (file)
RequestHandling
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
AsyncList
CodeActions
Completion
FileSource
GoTo
InfoUtils
References
Requests
Snapshots
Utils
Watchdog
Util (file)
CollectFVars
CollectLevelParams
CollectMVars
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
InstantiateLevelParams
MonadBacktrack
MonadCache
OccursCheck
PPExt
Path
Paths
Profile
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SCC
ShareCommon
Sorry
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
UserWidget
Attributes
AuxRecursor
Class
CoreM
Declaration
DeclarationRange
DocString
Environment
Eval
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LazyInitExtension
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
ProjFns
ReducibilityAttrs
ResolveName
Runtime
ScopedEnvExtension
Structure
SubExpr
Syntax
ToExpr
Mathlib (file)
Algebra
Algebra
Subalgebra
Basic
Pointwise
Tower
Unitization
Basic
Bilinear
Equiv
Hom
NonUnitalHom
NonUnitalSubalgebra
Operations
Opposite
Pi
Prod
RestrictScalars
Spectrum
Tower
Unitization
BigOperators
Multiset
Basic
Lemmas
Associated
Basic
Fin
Finprod
Finsupp
Intervals
NatAntidiagonal
Option
Order
Pi
Ring
RingEquiv
Category
AlgebraCat
Basic
Limits
Monoidal
Symmetric
FGModuleCat
Basic
Limits
GroupCat
Abelian
Adjunctions
Basic
Biproducts
Colimits
EpiMono
EquivalenceGroupAddGroup
FilteredColimits
Images
Injective
Kernels
Limits
Preadditive
Subobject
ZModuleEquivalence
Zero
ModuleCat
Monoidal
Basic
Closed
Symmetric
Abelian
Adjunctions
Algebra
Basic
Biproducts
ChangeOfRings
Colimits
EpiMono
FilteredColimits
Free
Images
Injective
Kernels
Limits
Presheaf
Products
Projective
Simple
Subobject
Tannaka
MonCat
Adjunctions
Basic
Colimits
FilteredColimits
Limits
Ring
Adjunctions
Basic
Colimits
Constructions
FilteredColimits
Instances
Limits
SemigroupCat
Basic
BoolRing
GroupWithZeroCat
CharP
Algebra
Basic
CharAndCard
ExpChar
Invertible
LocalRing
MixedCharZero
Pi
Quotient
Subring
Two
CharZero
Defs
Infinite
Lemmas
Quotient
ContinuedFractions
Computation
ApproximationCorollaries
Approximations
Basic
CorrectnessTerminating
TerminatesIffRat
Translations
Basic
ContinuantsRecurrence
ConvergentsEquiv
TerminatedStable
Translations
DirectSum
Algebra
Basic
Decomposition
Finsupp
Internal
LinearMap
Module
Ring
Divisibility
Basic
Prod
Units
EuclideanDomain
Basic
Defs
Instances
Field
Basic
Defs
IsField
MinimalAxioms
Opposite
Power
ULift
FreeMonoid
Basic
Count
GCDMonoid
Basic
Div
Finset
IntegrallyClosed
Multiset
Group
Commute
Basic
Defs
Hom
Units
Equiv
Basic
TypeTags
Hom
Basic
Defs
Instances
Semiconj
Basic
Defs
Units
Units (file)
Equiv
Hom
WithOne
Basic
Defs
Units
Aut
Basic
Commutator
Conj
ConjFinite
Defs
Embedding
Ext
Freiman
InjSurj
MinimalAxioms
Opposite
OrderSynonym
Pi
Prod
TypeTags
ULift
UniqueProds
GroupPower
Basic
CovariantClass
Identities
IterateHom
Lemmas
NegOnePow
Order
Ring
GroupRingAction
Basic
Invariant
Subobjects
GroupWithZero
Units
Basic
Equiv
Lemmas
Basic
Bitwise
Commute
Defs
Divisibility
InjSurj
NeZero
Power
Semiconj
Homology
HomotopyCategory (file)
HomComplex
Shift
ShortComplex
Ab
Abelian
Basic
ConcreteCategory
Exact
ExactFunctor
FunctorEquivalence
HomologicalComplex
Homology
LeftHomology
Limits
ModuleCat
Preadditive
PreservesHomology
QuasiIso
RightHomology
ShortExact
SnakeLemma
ShortExact
Abelian
Preadditive
Additive
Augment
ComplexShape
DifferentialObject
Exact
ExactSequence
Flip
Functor
HomologicalComplex
HomologicalComplexLimits
Homology
Homotopy
ImageToKernel
LocalCohomology
ModuleCat
Opposite
QuasiIso
Single
SingleHomology
Invertible
Basic
Defs
GroupWithZero
Jordan
Basic
Lie
Weights
Basic
Cartan
Linear
Abelian
BaseChange
Basic
CartanMatrix
CartanSubalgebra
Character
Classical
DirectSum
Engel
Free
IdealOperations
Killing
Matrix
Nilpotent
NonUnitalNonAssocAlgebra
Normalizer
OfAssociative
Quotient
Semisimple
SkewAdjoint
Solvable
Subalgebra
Submodule
TensorProduct
UniversalEnveloping
Module
Submodule
Basic
Bilinear
Lattice
LinearMap
Map
Pointwise
Algebra
Basic
BigOperators
Bimodule
DedekindDomain
Equiv
GradedModule
Hom
Injective
LinearMap
LocalizedModule
Opposites
PID
Pi
PointwisePi
Prod
Projective
Torsion
ULift
Zlattice
MonoidAlgebra
Basic
Degree
Division
Grading
Ideal
NoZeroDivisors
Support
ToDirectSum
Order
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Pi
Power
Group
Abs
Bounds
Defs
DenselyOrdered
InjSurj
Instances
MinMax
OrderIso
Prod
TypeTags
Units
WithTop
Hom
Basic
Monoid
Ring
Monoid
Canonical
Defs
WithZero
Basic
Defs
Basic
Defs
Lemmas
MinMax
NatCast
OrderDual
Prod
ToMulBot
TypeTags
Units
WithTop
Nonneg
Field
Floor
Module
Ring
Positive
Field
Ring
Ring
Abs
Canonical
CharZero
Cone
Defs
InjSurj
Lemmas
Star
WithTop
Sub
Basic
Canonical
Defs
Prod
WithTop
AbsoluteValue
Algebra
Archimedean
Chebyshev
CompleteField
EuclideanAbsoluteValue
Floor
Interval
Invertible
Kleene
LatticeGroup
Module
Monovary
Pi
Pointwise
Rearrangement
SMul
ToIntervalMod
UpperLower
WithZero
ZeroLEOne
Polynomial
BigOperators
GroupRingAction
Regular
Basic
Pow
SMul
Ring
Divisibility
Basic
Lemmas
Hom
Basic
Defs
AddAut
Aut
Basic
BooleanRing
CentroidHom
Commute
CompTypeclasses
Defs
Equiv
Fin
Idempotents
InjSurj
MinimalAxioms
Opposite
OrderSynonym
Pi
Prod
Regular
Semiconj
ULift
Units
Star
Basic
BigOperators
CHSH
Center
Free
Module
NonUnitalSubalgebra
Order
Pi
Pointwise
Prod
SelfAdjoint
StarAlgHom
Subalgebra
Unitary
Tropical
Basic
BigOperators
Lattice
Abs
AddTorsor
AlgebraicCard
Associated
Bounds
CovariantAndContravariant
CubicDiscriminant
DirectLimit
DualNumber
DualQuaternion
Exact
Expr
Free
FreeAlgebra
FreeNonUnitalNonAssocAlgebra
GeomSum
GradedMonoid
GradedMulAction
HierarchyDesign
IndicatorFunction
IsPrimePow
LinearRecurrence
ModEq
NeZero
Opposites
PEmptyInstances
PUnitInstances
Parity
Periodic
QuadraticDiscriminant
Quandle
Quaternion
QuaternionBasis
Quotient
RingQuot
SMulWithZero
Squarefree
Support
Symmetrized
TrivSqZeroExt
AlgebraicGeometry
EllipticCurve
Point
Weierstrass
Morphisms
Basic
FiniteType
OpenImmersion
QuasiCompact
QuasiSeparated
RingHomProperties
UniversallyClosed
PrimeSpectrum
Basic
IsOpenComapC
Maximal
Noetherian
ProjectiveSpectrum
Scheme
StructureSheaf
Topology
Sites
BigZariski
AffineScheme
FunctionField
GammaSpecAdjunction
Gluing
Limits
OpenImmersion
Properties
Pullbacks
Restrict
Scheme
Spec
StructureSheaf
AlgebraicTopology
DoldKan
Compatibility
Decomposition
Degeneracies
Equivalence
EquivalenceAdditive
EquivalencePseudoabelian
Faces
FunctorGamma
FunctorN
GammaCompN
Homotopies
HomotopyEquivalence
NCompGamma
NReflectsIso
Normalized
Notations
PInfty
Projections
SplitSimplicialObject
FundamentalGroupoid
Basic
FundamentalGroup
InducedMaps
PUnit
Product
SimplyConnected
AlternatingFaceMapComplex
CechNerve
ExtraDegeneracy
MooreComplex
Nerve
SimplexCategory
SimplicialObject
SimplicialSet
SplitSimplicialObject
TopologicalSimplex
Analysis
Analytic
Basic
Composition
Constructions
Inverse
IsolatedZeros
Linear
RadiusLiminf
Uniqueness
Asymptotics
AsymptoticEquivalent
Asymptotics
SpecificAsymptotics
SuperpolynomialDecay
Theta
BoxIntegral
Box
Basic
SubboxInduction
Partition
Additive
Basic
Filter
Measure
Split
SubboxInduction
Tagged
Basic
DivergenceTheorem
Integrability
Calculus
BumpFunction
Basic
Convolution
FiniteDimension
InnerProduct
Normed
Conformal
InnerProduct
NormedSpace
ContDiff
Basic
Bounds
Defs
FiniteDimension
IsROrC
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
Mul
Pi
Polynomial
Pow
Prod
Slope
Star
Support
ZPow
FDeriv
Add
Analytic
Basic
Bilinear
Comp
Equiv
Extend
Linear
Measurable
Mul
Pi
Prod
RestrictScalars
Star
Symmetric
Gradient
Basic
LineDeriv
Basic
Measurable
LocalExtr
Basic
Polynomial
Rolle
AffineMap
Darboux
DiffContOnCl
Dslope
FormalMultilinearSeries
Implicit
Inverse
IteratedDeriv
LHopital
LagrangeMultipliers
MeanValue
Monotone
ParametricIntegral
ParametricIntervalIntegral
Rademacher
Series
TangentCone
Taylor
UniformLimitsDeriv
Complex
UnitDisc
Basic
UpperHalfPlane
Basic
FunctionsBoundedAtInfty
Manifold
Metric
Topology
AbsMax
Arg
Basic
CauchyIntegral
Circle
Conformal
Isometry
Liouville
LocallyUniformLimit
OpenMapping
OperatorNorm
PhragmenLindelof
Polynomial
ReImTopology
RealDeriv
RemovableSingularity
Schwarz
Convex
Cone
Basic
Dual
Extension
Pointed
Proper
SimplicialComplex
Basic
SpecificFunctions
Basic
Deriv
Pow
Basic
Between
Body
Caratheodory
Combination
Complex
Contractible
Exposed
Extrema
Extreme
Function
Gauge
Hull
Independent
Integral
Intrinsic
Jensen
Join
KreinMilman
Measure
Mul
Normed
PartitionOfUnity
Quasiconvex
Radon
Segment
Side
Slope
Star
StoneSeparation
Strict
StrictConvexBetween
StrictConvexSpace
Strong
Topology
Uniform
Distribution
AEEqOfIntegralContDiff
SchwartzSpace
Fourier
AddCircle
FourierTransform
PoissonSummation
RiemannLebesgueLemma
InnerProductSpace
Adjoint
Basic
Calculus
ConformalLinearMap
Dual
EuclideanDist
GramSchmidtOrtho
LaxMilgram
LinearPMap
MeanErgodic
OfNorm
Orientation
Orthogonal
PiL2
Positive
ProdL2
Projection
Rayleigh
Spectrum
Symmetric
TwoDim
l2Space
LocallyConvex
AbsConvex
BalancedCoreHull
Barrelled
Basic
Bounded
ContinuousOfBounded
Polar
StrongTopology
WeakDual
WithSeminorms
Normed
Field
Basic
InfiniteSum
UnitBall
Group
SemiNormedGroupCat (file)
Completion
Kernels
AddCircle
AddTorsor
BallSphere
Basic
Completion
ControlledClosure
Hom
HomCompletion
InfiniteSum
Pointwise
Quotient
Seminorm
Order
Basic
Lattice
UpperLower
Ring
Seminorm
MulAction
NormedSpace
HahnBanach
Extension
SeparatingDual
Separation
Star
Basic
ContinuousFunctionalCalculus
Exponential
GelfandDuality
Matrix
Multiplier
Spectrum
Unitization
AddTorsor
AddTorsorBases
AffineIsometry
Algebra
BallAction
Banach
BanachSteinhaus
Basic
BoundedLinearMaps
CompactOperator
Complemented
Completion
ConformalLinearMap
Connected
ContinuousAffineMap
ContinuousLinearMap
Dual
DualNumber
ENorm
Exponential
Extend
Extr
FiniteDimension
HomeomorphBall
IndicatorFunction
Int
IsROrC
LinearIsometry
LpEquiv
MStructure
MatrixExponential
MazurUlam
Multilinear
MultilinearCurrying
OperatorNorm
PiLp
Pointwise
ProdLp
QuaternionExponential
Ray
RieszLemma
Spectrum
SphereNormEquiv
TrivSqZeroExt
Unitization
Units
WeakDual
WithLp
lpSpace
ODE
Gronwall
PicardLindelof
SpecialFunctions
Complex
Arg
Circle
Log
LogDeriv
Gamma
Basic
Beta
BohrMollerup
Log
Base
Basic
Deriv
Monotone
Pow
Asymptotics
Complex
Continuity
Deriv
NNReal
Real
Trigonometric
Angle
Arctan
ArctanDeriv
Basic
Bounds
Chebyshev
Complex
ComplexDeriv
Deriv
EulerSineProd
Inverse
InverseDeriv
Series
Arsinh
Bernstein
CompareExp
Exp
ExpDeriv
Exponential
Gaussian
ImproperIntegrals
Integrals
JapaneseBracket
NonIntegrable
PolarCoord
PolynomialExp
Polynomials
SmoothTransition
Sqrt
Stirling
SpecificLimits
Basic
FloorPow
IsROrC
Normed
VonNeumannAlgebra
Basic
BoundedVariation
ConstantSpeed
Convolution
Hofer
Matrix
MeanInequalities
MeanInequalitiesPow
MellinTransform
PSeries
Quaternion
Seminorm
Subadditive
SumIntegralComparisons
CategoryTheory
Abelian
DiagramLemmas
Four
Basic
Exact
Ext
FunctorCategory
Generator
Homology
Images
Injective
InjectiveResolution
LeftDerived
NonPreadditive
Opposite
Projective
Pseudoelements
Refinements
RightDerived
Subobject
Transfer
Adjunction
AdjointFunctorTheorems
Basic
Comma
Evaluation
FullyFaithful
Lifting
Limits
Mates
Opposites
Over
Reflective
Whiskering
Bicategory
Adjunction
Basic
Coherence
End
Extension
Free
Functor
FunctorBicategory
IsKan
LocallyDiscrete
NaturalTransformation
SingleObj
Strict
Category
Cat (file)
Limit
Basic
Bipointed
Factorisation
GaloisConnection
Grpd
Init
KleisliCat
Pairwise
PartialFun
Pointed
Preorder
Quiv
RelCat
TwoP
ULift
Closed
Cartesian
Functor
FunctorCategory
Ideal
Monoidal
Types
Zero
ConcreteCategory
Basic
Bundled
BundledHom
Elementwise
ReflectsIso
UnbundledHom
Endofunctor
Algebra
Enriched
Basic
Filtered
Basic
Small
Functor
Basic
Category
Const
Currying
EpiMono
Flat
FullyFaithful
Functorial
Hom
InvIsos
LeftDerived
ReflectsIso
Trifunctor
GradedObject (file)
Bifunctor
Groupoid (file)
Basic
FreeGroupoid
Subgroupoid
VertexGroup
Idempotents
Basic
Biproducts
FunctorCategories
FunctorExtension
HomologicalComplex
Karoubi
KaroubiKaroubi
SimplicialObject
LiftingProperties
Adjunction
Basic
Limits
Constructions
Over
Basic
Connected
Products
BinaryProducts
EpiMono
Equalizers
Filtered
FiniteProductsOfBinaryProducts
LimitsOfProductsAndEqualizers
Pullbacks
WeaklyInitial
ZeroObjects
Preserves
Shapes
BinaryProducts
Biproducts
Equalizers
Images
Kernels
Products
Pullbacks
Terminal
Zero
Basic
Filtered
Finite
FunctorCategory
Limits
Opposites
Ulift
Shapes
NormalMono
Basic
Equalizers
BinaryProducts
Biproducts
CommSq
ConcreteCategory
Diagonal
DisjointCoproduct
Equalizers
Equivalence
FiniteLimits
FiniteProducts
FunctorCategory
Images
KernelPair
Kernels
Multiequalizer
Products
Pullbacks
Reflexive
RegularMono
SplitCoequalizer
StrictInitial
StrongEpi
Terminal
Types
WideEqualizers
WidePullbacks
ZeroMorphisms
ZeroObjects
Bicones
ColimitLimit
Comma
ConcreteCategory
ConeCategory
Cones
Connected
Creates
EssentiallySmall
ExactFunctor
Filtered
FilteredColimitCommutesFiniteLimit
Final
FinallySmall
FintypeCat
Fubini
FullSubcategory
FunctorCategory
HasLimits
IsLimit
KanExtension
Lattice
MonoCoprod
Opposites
Over
Pi
Presheaf
SmallComplete
Types
Unit
VanKampen
Yoneda
Linear
Basic
FunctorCategory
LinearFunctor
Yoneda
Localization
Adjunction
CalculusOfFractions
Composition
Construction
Equivalence
LocalizerMorphism
Opposite
Predicate
Prod
Monad
Adjunction
Algebra
Basic
Coequalizer
EquivMon
Kleisli
Limits
Monadicity
Products
Types
Monoidal
Free
Basic
Coherence
Internal
FunctorCategory
Limits
Module
Types
OfChosenFiniteProducts
Basic
Symmetric
Rigid
Basic
FunctorCategory
OfEquivalence
Types
Basic
Coyoneda
Symmetric
Bimod
Braided
Category
Center
CoherenceLemmas
CommMon_
Discrete
End
Functor
FunctorCategory
Functorial
Limits
Linear
Mod_
Mon_
NaturalTransformation
OfHasFiniteProducts
Opposite
Preadditive
Skeleton
Subcategory
Tor
Transport
Pi
Basic
Preadditive
Yoneda
Basic
Injective
Limits
Projective
AdditiveFunctor
Basic
Biproducts
EilenbergMoore
EndoFunctor
FunctorCategory
Generator
HomOrthogonal
Injective
InjectiveResolution
LeftExact
Mat
OfBiproducts
Opposite
Projective
ProjectiveResolution
Schur
SingleObj
Products
Associator
Basic
Bifunctor
Quotient (file)
Preadditive
Shift
Basic
CommShift
Induced
Localization
Opposite
Pullback
Quotient
Sigma
Basic
Sites
Adjunction
Canonical
Closed
Coherent
CompatiblePlus
CompatibleSheafification
ConstantSheaf
CoverLifting
CoverPreserving
Coverage
DenseSubsite
EffectiveEpimorphic
EqualizerSheafCondition
Grothendieck
InducedTopology
IsSheafFor
LeftExact
Limits
Over
Plus
Preserves
Pretopology
Pullback
RegularExtensive
Sheaf
SheafHom
SheafOfTypes
Sheafification
Sieves
Spaces
Subsheaf
Surjective
Types
Whiskering
Subobject
Basic
Comma
FactorThru
Lattice
Limits
MonoOver
Types
WellPowered
Sums
Associator
Basic
Triangulated
Basic
Opposite
Pretriangulated
Rotate
TriangleShift
Triangulated
Action
Adhesive
Arrow
Balanced
CatCommSq
CofilteredSystem
CommSq
Comma
ComposableArrows
Conj
ConnectedComponents
Core
DifferentialObject
DiscreteCategory
Elements
Elementwise
Endomorphism
EpiMono
EqToHom
Equivalence
EssentialImage
EssentiallySmall
Extensive
FinCategory
FintypeCat
FullSubcategory
Generator
GlueData
Grothendieck
IsConnected
Iso
IsomorphismClasses
MorphismProperty
NatIso
NatTrans
Noetherian
Opposites
Over
PEmpty
PUnit
PathCategory
Simple
SingleObj
Skeletal
StructuredArrow
Subterminal
Thin
Types
UnivLE
Whiskering
WithTerminal
Yoneda
Combinatorics
Additive
Behrend
ETransform
Energy
PluenneckeRuzsa
RuzsaCovering
SalemSpencer
Derangements
Basic
Exponential
Finite
Hall
Basic
Finite
Optimization
ValuedCSP
Quiver
Arborescence
Basic
Cast
ConnectedComponent
Covering
Path
Push
SingleObj
Subquiver
Symmetric
SetFamily
Compression
Down
UV
FourFunctions
HarrisKleitman
Intersecting
Kleitman
LYM
Shadow
Shatter
SimpleGraph
Connectivity (file)
Subgraph
Ends
Defs
Properties
Regularity
Bound
Chunk
Energy
Equitabilise
Increment
Lemma
Uniform
Triangle
Basic
Acyclic
AdjMatrix
Basic
Clique
Coloring
ConcreteColorings
DegreeSum
Density
Finsubgraph
Girth
Hasse
IncMatrix
Init
Matching
Metric
Partition
Prod
StronglyRegular
Subgraph
Trails
Young
SemistandardTableau
YoungDiagram
Catalan
Colex
Composition
Configuration
DoubleCounting
HalesJewett
Hindman
Partition
Pigeonhole
Computability
AkraBazzi
AkraBazzi
GrowsPolynomially
Ackermann
ContextFreeGrammar
DFA
Encoding
EpsilonNFA
Halting
Language
NFA
Partrec
PartrecCode
Primrec
Reduce
RegularExpressions
TMComputable
TMToPartrec
TuringMachine
Condensed
Abelian
Adjunctions
Basic
Discrete
Equivalence
Functors
Limits
Solid
Control
Bitraversable
Basic
Instances
Lemmas
EquivFunctor (file)
Instances
Functor (file)
Multivariate
Monad
Basic
Cont
Writer
Traversable
Basic
Equiv
Instances
Lemmas
Applicative
Basic
Bifunctor
Fix
Fold
LawfulFix
Random
ULift
ULiftable
Data
Analysis
Filter
Topology
Array
Basic
Defs
Lemmas
Bitvec
Defs
Lemmas
Bool
AllAny
Basic
Count
Set
Buffer
Parser
Basic
Numeral
Basic
Complex
Abs
Basic
BigOperators
Cardinality
Determinant
Exponential
ExponentialBounds
Module
Order
Orientation
Countable
Basic
Defs
Small
DFinsupp
Basic
Encodable
Interval
Lex
Multiset
NeLocus
Order
WellFounded
DList
Basic
Defs
Instances
ENat
Basic
Lattice
Equiv
Functor
FP
Basic
Fin
Tuple
Basic
BubbleSortInduction
Curry
Monotone
NatAntidiagonal
Reflection
Sort
Basic
Fin2
FlagRange
Interval
SuccPred
VecNotation
Finite
Basic
Card
Defs
Set
Finset
Antidiagonal
Basic
Card
Fin
Finsupp
Fold
Functor
Image
Interval
Lattice
LocallyFinite
MulAntidiagonal
NAry
NatAntidiagonal
NoncommProd
Option
Order
PImage
Pairwise
Pi
PiInduction
Pointwise
Powerset
Preimage
Prod
Sigma
Slice
Sort
Sum
Sups
Sym
Update
Finsupp
AList
Antidiagonal
Basic
BigOperators
Defs
Encodable
Fin
Fintype
Indicator
Interval
Lex
Multiset
NeLocus
Notation
Order
Pointwise
Pwo
ToDFinsupp
WellFounded
Fintype
Array
Basic
BigOperators
Card
CardEmbedding
Fin
Lattice
List
Option
Order
Parity
Perm
Pi
Powerset
Prod
Quotient
Sigma
Small
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Fintype
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Dvd
Basic
Pow
Order
Basic
Lemmas
Units
AbsoluteValue
Associated
Basic
Bitwise
CharZero
ConditionallyCompleteOrder
Div
GCD
Interval
LeastGreatest
Lemmas
Log
ModEq
NatPrime
Parity
Range
Sqrt
SuccPred
Units
IsROrC
Basic
Lemmas
LazyList (file)
Basic
List
BigOperators
Basic
Lemmas
EditDistance
Bounds
Defs
Estimator
AList
Basic
Card
Chain
Count
Cycle
Dedup
Defs
Destutter
DropRight
Duplicate
FinRange
Forall2
Func
Indexes
Infix
Intervals
Join
Lattice
Lemmas
Lex
MinMax
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
ProdSigma
Range
Rotate
Sections
Sigma
Sort
Sublists
Sym
TFAE
ToFinsupp
Zip
MLList
Basic
BestFirst
Dedup
DepthFirst
IO
Split
Matrix
Auto
Basic
Basis
Block
CharP
ColumnRowPartitioned
DMatrix
DualNumber
Hadamard
Invertible
Kronecker
Notation
PEquiv
Rank
Reflection
RowCol
Matroid
Basic
IndepAxioms
Init
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fintype
Fold
Functor
Interval
Lattice
LocallyFinite
NatAntidiagonal
Nodup
Pi
Powerset
Range
Sections
Sort
Sum
Sym
MvPolynomial
Basic
Cardinal
Comap
CommRing
Counit
Derivation
Division
Equiv
Expand
Funext
Invertible
Monad
PDeriv
Polynomial
Rename
Supported
Variables
Nat
Cast
Basic
Commute
Defs
Field
NeZero
Order
Prod
Synonym
WithTop
Choose
Basic
Bounds
Cast
Central
Dvd
Factorization
Multinomial
Sum
Vandermonde
Factorial
Basic
BigOperators
Cast
DoubleFactorial
SuperFactorial
Factorization
Basic
PrimePow
Fib
Basic
Zeckendorf
GCD
Basic
BigOperators
Order
Basic
Lemmas
Basic
Bits
Bitwise
Count
Digits
Dist
EvenOddRec
Factors
ForSqrt
Hyperoperation
Interval
Lattice
Log
MaxPowDiv
ModEq
Multiplicity
Nth
PSub
Pairing
Parity
PartENat
Periodic
Pow
Prime
PrimeFin
PrimeNormNum
Set
Size
Sqrt
SqrtNormNum
Squarefree
SuccPred
Totient
Units
Upto
WithBot
Nondet
Basic
Num
Basic
Bitwise
Lemmas
Prime
Option
Basic
Defs
NAry
Ordmap
Ordnode
Ordset
PFunctor
Multivariate
Basic
M
W
Univariate
Basic
M
PNat
Basic
Defs
Factors
Find
Interval
Prime
Xgcd
PSigma
Order
Pi
Algebra
Interval
Lex
Polynomial
Degree
CardPowDegree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
CancelLeads
Cardinal
Coeff
DenomsClearable
Derivation
Derivative
Div
EraseLead
Eval
Expand
FieldDivision
HasseDeriv
Identities
Induction
Inductions
Laurent
Lifts
Mirror
Module
Monic
Monomial
PartialFractions
Reverse
RingDivision
Splits
Taylor
UnitTrinomial
Prod
Basic
Lex
PProd
TProd
QPF
Multivariate
Constructions
Cofix
Comp
Const
Fix
Prj
Quot
Sigma
Basic
Univariate
Basic
Rat
Cast
CharZero
Defs
Lemmas
Order
Basic
BigOperators
Defs
Denumerable
Encodable
Floor
Init
Lemmas
NNRat
Order
Sqrt
Star
Rbmap
Basic
Default
Rbtree
Basic
DefaultLt
Find
Init
Insert
Main
MinMax
Real
Pi
Bounds
Leibniz
Wallis
Archimedean
Basic
Cardinality
CauSeq
CauSeqCompletion
ConjugateExponents
ENNReal
ENatENNReal
EReal
GoldenRatio
Hyperreal
Irrational
NNReal
Pointwise
Sign
Sqrt
Seq
Computation
Parallel
Seq
WSeq
Set
Intervals
Basic
Disjoint
Group
Image
Infinite
Instances
IsoIoo
Monoid
Monotone
OrdConnected
OrdConnectedComponent
OrderIso
Pi
ProjIcc
SurjOn
UnorderedInterval
WithBotTop
Pairwise
Basic
Lattice
Pointwise
Basic
BigOperators
Finite
Interval
Iterate
ListOfFn
SMul
Support
Accumulate
Basic
BoolIndicator
Card
Constructions
Countable
Enumerate
Equitable
Finite
Function
Functor
Image
Lattice
List
MulAntidiagonal
NAry
Opposite
Prod
Semiring
Sigma
Sups
UnionLift
SetLike
Basic
Fintype
Setoid
Basic
Partition
Sigma
Basic
Interval
Lex
Order
Stream
Defs
Init
String
Basic
Defs
Lemmas
Sum
Basic
Interval
Lattice
Order
Sym
Sym2 (file)
Init
Basic
Card
Vector (file)
Basic
MapLemmas
Mem
Snoc
Zip
W
Basic
Cardinal
Constructions
ZMod
Algebra
Basic
Coprime
Defs
IntUnitsPower
Parity
Quotient
Units
BinaryHeap
Bracket
Bundle
ByteArray
Char
Erased
FinEnum
Finmap
HashMap
Holor
Opposite
PEquiv
PFun
Part
Quot
Rel
SProd
Semiquot
Sign
Subtype
Tree
TwoPointing
TypeMax
TypeVec
UInt
ULift
UnionFind
Vector3
Deprecated
Group
Ring
Subfield
Subgroup
Submonoid
Subring
Dynamics
BirkhoffSum
Average
Basic
NormedSpace
Circle
RotationNumber
TranslationNumber
Ergodic
AddCircle
Conservative
Ergodic
Function
MeasurePreserving
FixedPoints
Basic
Topology
Flow
Minimal
OmegaLimit
PeriodicPts
FieldTheory
Finite
Basic
GaloisField
Polynomial
Trace
IsAlgClosed
AlgebraicClosure
Basic
Classification
Spectrum
Minpoly
Basic
Field
IsIntegrallyClosed
SplittingField
Construction
IsSplittingField
AbelRuffini
AbsoluteGaloisGroup
Adjoin
AxGrothendieck
Cardinality
ChevalleyWarning
Finiteness
Fixed
Galois
IntermediateField
IsSepClosed
KrullTopology
Laurent
MvPolynomial
Normal
NormalClosure
Perfect
PerfectClosure
PolynomialGaloisGroup
PrimitiveElement
RatFunc
Separable
SeparableDegree
Subfield
Tower
Geometry
Euclidean
Angle
Oriented
Affine
Basic
RightAngle
Rotation
Unoriented
Affine
Basic
Conformal
RightAngle
Sphere
Inversion
Basic
Calculus
ImageHyperplane
Sphere
Basic
Power
Ptolemy
SecondInter
Basic
Circumcenter
MongePoint
PerpBisector
Triangle
Manifold
Algebra
LeftInvariantDerivation
LieGroup
Monoid
SmoothFunctions
Structures
Instances
Real
Sphere
UnitsOfNormedAlgebra
Sheaf
Basic
LocallyRingedSpace
Smooth
VectorBundle
Basic
FiberwiseLinear
Hom
Pullback
SmoothSection
Tangent
BumpFunction
ChartedSpace
Complex
ConformalGroupoid
ContMDiff
ContMDiffMFDeriv
ContMDiffMap
DerivationBundle
Diffeomorph
LocalInvariantProperties
MFDeriv
Metrizable
PartitionOfUnity
SmoothManifoldWithCorners
WhitneyEmbedding
RingedSpace
LocallyRingedSpace (file)
HasColimits
PresheafedSpace (file)
Gluing
HasColimits
Basic
OpenImmersion
SheafedSpace
Stalks
GroupTheory
Coprod
Basic
FreeGroup
Basic
IsFreeGroup
NielsenSchreier
GroupAction
DomAct
ActionHom
Basic
SubMulAction (file)
Pointwise
Basic
BigOperators
ConjAct
Defs
Embedding
FixingSubgroup
Group
Hom
Opposite
Option
Pi
Prod
Quotient
Sigma
Sum
Support
Units
Order
Min
Perm
Cycle
Basic
Concrete
PossibleTypes
Type
Basic
Fin
List
Option
Sign
Subgroup
Support
ViaEmbedding
SpecificGroups
Alternating
Cyclic
Dihedral
KleinFour
Quaternion
Subgroup
Actions
Basic
Finite
MulOpposite
Pointwise
Saturated
Simple
ZPowers
Submonoid
Basic
Center
Centralizer
Inverses
Membership
MulOpposite
Operations
Pointwise
ZeroDivisors
Subsemigroup
Basic
Center
Centralizer
Membership
Operations
Abelianization
Archimedean
ClassEquation
Commensurable
Commutator
CommutingProbability
Complement
Congruence
CoprodI
Coset
Divisible
DoubleCoset
EckmannHilton
Exponent
FiniteAbelian
Finiteness
FreeAbelianGroup
FreeAbelianGroupFinsupp
HNNExtension
Index
MonoidLocalization
Nilpotent
NoncommPiCoprod
OrderOfElement
PGroup
PresentedGroup
PushoutI
QuotientGroup
Schreier
SchurZassenhaus
SemidirectProduct
Solvable
Sylow
Torsion
Transfer
InformationTheory
Hamming
Init
Algebra
Classes
Classes
Order
Control
Combinators
Lawful
Data
Bool
Basic
Lemmas
Buffer
Parser
Fin
Basic
Int
Basic
Bitwise
CompLemmas
DivMod
Lemmas
Order
List
Basic
Instances
Lemmas
Nat
Basic
Bitwise
Div
GCD
Lemmas
Notation
Option
Init
Lemmas
Basic
Lemmas
Ordering
Basic
Lemmas
Rat
Basic
Sigma
Basic
Lex
Subtype
Basic
Prod
Quot
Meta
WellFoundedTactics
Order
Defs
LinearOrder
Align
CCLemmas
Classical
Core
Function
IteSimp
Logic
Propext
Quot
Set
ZeroOne
Lean
Data
NameMap
Elab
Tactic
Basic
Term
Expr (file)
Basic
ExtraRecognizers
ReplaceRec
Traverse
IO
Process
Meta (file)
Basic
CongrTheorems
DiscrTree
Simp
PrettyPrinter
Delaborator
System
IO
CoreM
EnvExtension
Exception
Json
LocalContext
Message
Name
SMap
Thunk
LinearAlgebra
AffineSpace
AffineEquiv
AffineMap
AffineSubspace
Basic
Basis
Combination
FiniteDimensional
Independent
Matrix
Midpoint
MidpointZero
Ordered
Pointwise
Restrict
Slope
Alternating
Basic
DomCoprod
Basis (file)
Bilinear
Flag
VectorSpace
BilinearForm (file)
TensorProduct
Charpoly
Basic
ToMatrix
CliffordAlgebra
BaseChange
Basic
CategoryTheory
Conjugation
Contraction
Equivs
Even
EvenEquiv
Fold
Grading
Star
DirectSum
Finsupp
TensorProduct
Eigenspace
Basic
Minpoly
Triangularizable
ExteriorAlgebra
Basic
Grading
OfAlternating
FreeModule
Finite
Basic
Matrix
Rank
Basic
Determinant
IdealQuotient
Norm
PID
Rank
StrongRankCondition
Matrix
Charpoly
Basic
Coeff
Eigs
FiniteField
LinearMap
Minpoly
AbsoluteValue
Adjugate
Basis
BilinearForm
Block
Circulant
Determinant
Diagonal
DotProduct
Dual
FiniteDimensional
GeneralLinearGroup
Gershgorin
Hermitian
InvariantBasisNumber
IsDiag
LDL
MvPolynomial
Nondegenerate
NonsingularInverse
Orthogonal
Polynomial
PosDef
Reindex
SchurComplement
SesquilinearForm
SpecialLinearGroup
Spectrum
Symmetric
ToLin
ToLinearEquiv
Trace
Transvection
ZPow
Multilinear
Basic
Basis
FiniteDimensional
TensorProduct
Projectivization
Basic
Independence
Subspace
QuadraticForm
QuadraticModuleCat (file)
Monoidal
Symmetric
TensorProduct (file)
Isometries
Basic
Complex
Dual
Isometry
IsometryEquiv
Prod
Real
TensorAlgebra
Basic
Basis
Grading
ToTensorPower
TensorProduct (file)
Matrix
Opposite
Prod
RightExactness
Tower
AdicCompletion
AnnihilatingPolynomial
Basic
BilinearMap
Coevaluation
Contraction
CrossProduct
DFinsupp
Determinant
Dimension
Dual
FiniteDimensional
Finrank
Finsupp
FinsuppVectorSpace
FreeAlgebra
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
Lagrange
LinearIndependent
LinearPMap
Orientation
PID
PerfectPairing
Pi
PiTensorProduct
Prod
Projection
Quotient
QuotientPi
Ray
SModEq
SesquilinearForm
Span
StdBasis
SymplecticGroup
TensorPower
TensorProductBasis
Trace
UnitaryGroup
Vandermonde
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Array
Basic
Defs
Embedding
Fin
Fintype
Functor
List
LocalEquiv
Nat
Option
Set
TransferInstance
Function
Basic
Conjugate
Iterate
OfArity
Nontrivial
Basic
Defs
Small
Basic
Defs
Group
List
Module
Ring
Basic
Denumerable
Hydra
IsEmpty
Lemmas
Nonempty
Pairwise
Relation
Relator
Unique
UnivLE
Mathport
Attributes
Notation
Rename
Syntax
MeasureTheory
Category
MeasCat
Constructions
BorelSpace
Basic
Complex
ContinuousLinearMap
Metrizable
Prod
Basic
Integral
HaarToSphere
Pi
Polish
Covering
Besicovitch
BesicovitchVectorSpace
DensityTheorem
Differentiation
LiminfLimsup
OneDim
Vitali
VitaliFamily
Decomposition
Jordan
Lebesgue
RadonNikodym
SignedHahn
SignedLebesgue
UnsignedHahn
Function
AEEqFun (file)
DomAct
ConditionalExpectation
AEMeasurable
Basic
CondexpL1
CondexpL2
Indicator
Real
Unique
LpSpace (file)
DomAct
Basic
SpecialFunctions
Arctan
Basic
Inner
IsROrC
StronglyMeasurable
Basic
Inner
Lp
AEEqOfIntegral
AEMeasurableOrder
AEMeasurableSequence
ContinuousMapDense
ConvergenceInMeasure
Egorov
EssSup
Floor
Jacobian
L1Space
L2Space
LocallyIntegrable
LpOrder
LpSeminorm
SimpleFunc
SimpleFuncDense
SimpleFuncDenseLp
UniformIntegrable
Group
Action
AddCircle
Arithmetic
FundamentalDomain
GeometryOfNumbers
Integral
LIntegral
MeasurableEquiv
Measure
Pointwise
Prod
Integral
Average
Bochner
BoundedContinuousFunction
CircleIntegral
CircleTransform
DivergenceTheorem
ExpDecay
FundThmCalculus
Indicator
IntegrableOn
IntegralEqImproper
IntervalAverage
IntervalIntegral
Layercake
Lebesgue
LebesgueNormedSpace
MeanInequalities
PeakFunction
Periodic
RieszMarkovKakutani
SetIntegral
SetToL1
TorusIntegral
VitaliCaratheodory
MeasurableSpace
Basic
Card
Defs
Invariants
Measure
Haar
Basic
Disintegration
InnerProductSpace
NormedSpace
OfBasis
Quotient
Unique
Lebesgue
Basic
Complex
EqHaar
Integral
AEDisjoint
AEMeasurable
Complex
Content
Count
Dirac
Doubling
FiniteMeasure
GiryMonad
Hausdorff
MeasureSpace
MeasureSpaceDef
MutuallySingular
NullMeasurable
OpenPos
OuterMeasure
Portmanteau
ProbabilityMeasure
Regular
Restrict
Stieltjes
Sub
Trim
Typeclasses
VectorMeasure
WithDensity
WithDensityVectorMeasure
Lattice
PiSystem
Tactic
ModelTheory
Algebra
Field
Basic
CharP
Ring
Basic
FreeCommRing
Basic
Bundled
Definability
DirectLimit
ElementaryMaps
Encoding
FinitelyGenerated
Fraisse
Graph
LanguageMap
Order
Quotients
Satisfiability
Semantics
Skolem
Substructures
Syntax
Types
Ultraproducts
NumberTheory
ClassNumber
AdmissibleAbs
AdmissibleAbsoluteValue
AdmissibleCardPowDegree
Finite
FunctionField
Cyclotomic
Basic
Discriminant
Gal
PrimitiveRoots
Rat
DirichletCharacter
Basic
Bounds
EulerProduct
Basic
FLT
Basic
Four
LegendreSymbol
QuadraticChar
Basic
GaussSum
AddCharacter
Basic
GaussEisensteinLemmas
GaussSum
JacobiSymbol
MulCharacter
QuadraticReciprocity
ZModChar
Liouville
Basic
LiouvilleNumber
LiouvilleWith
Measure
Residual
ModularForms
JacobiTheta
Basic
Manifold
Basic
CongruenceSubgroups
SlashActions
SlashInvariantForms
NumberField
Basic
CanonicalEmbedding
ClassNumber
Discriminant
Embeddings
Norm
Units
Padics
Harmonic
Hensel
PadicIntegers
PadicNorm
PadicNumbers
PadicVal
RingHoms
Zsqrtd
Basic
GaussianInt
QuadraticReciprocity
ToReal
ADEInequality
ArithmeticFunction
Basic
Bernoulli
BernoulliPolynomials
Bertrand
Dioph
DiophantineApproximation
Divisors
FermatPsp
FrobeniusNumber
FunctionField
KummerDedekind
LSeries
LucasLehmer
LucasPrimality
Modular
Multiplicity
Pell
PellMatiyasevic
PrimeCounting
PrimesCongruentOne
Primorial
PythagoreanTriples
RamificationInertia
Rayleigh
SmoothNumbers
SumFourSquares
SumTwoSquares
VonMangoldt
WellApproximable
Wilson
ZetaFunction
ZetaValues
Order
Atoms (file)
Finite
Bounds
Basic
OrderIso
Category
BddDistLat
BddLat
BddOrd
BoolAlg
CompleteLat
DistLat
FinBddDistLat
FinBoolAlg
FinPartOrd
Frm
HeytAlg
Lat
LinOrd
NonemptyFinLinOrd
OmegaCompletePartialOrder
PartOrd
Preord
Semilat
ConditionallyCompleteLattice
Basic
Finset
Group
Extension
Linear
Well
Filter
Archimedean
AtTopBot
Bases
Basic
Cofinite
CountableInter
CountableSeparatingOn
Curry
ENNReal
EventuallyConst
Extr
FilterProduct
Germ
IndicatorFunction
Interval
Lift
ModEq
NAry
Partial
Pi
Pointwise
Prod
SmallSets
Subsingleton
Ultrafilter
ZeroAndBoundedAtFilter
Heyting
Basic
Boundary
Hom
Regular
Hom
Basic
Bounded
CompleteLattice
Lattice
Order
Set
Monotone
Basic
Extension
Monovary
Odd
Union
Partition
Equipartition
Finpartition
RelIso
Basic
Group
Set
SuccPred
Basic
IntervalSucc
Limit
LinearLocallyFinite
Relation
UpperLower
Basic
Hom
LocallyFinite
Antichain
Antisymmetrization
Basic
Birkhoff
BooleanAlgebra
Booleanisation
Bounded
BoundedOrder
Chain
Circular
Closure
CompactlyGenerated
Compare
CompleteBooleanAlgebra
CompleteLattice
CompleteLatticeIntervals
CompletePartialOrder
Concept
Copy
CountableDenseLinearOrder
Cover
Directed
Disjoint
Disjointed
Estimator
FixedPoints
GaloisConnection
GameAdd
Grade
Height
Ideal
InitialSeg
Interval
Irreducible
Iterate
JordanHolder
KrullDimension
Lattice
LatticeIntervals
LiminfLimsup
LocallyFinite
Max
MinMax
Minimal
ModularLattice
OmegaCompletePartialOrder
OrdContinuous
OrderIsoNat
PFilter
PartialSups
PrimeIdeal
PropInstances
RelClasses
RelSeries
SemiconjSup
Sublattice
SupClosed
SupIndep
SymmDiff
Synonym
ULift
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
Probability
Distributions
Exponential
Gaussian
Independence
Basic
Kernel
ZeroOne
Kernel
Basic
Composition
CondCdf
CondDistrib
Condexp
Disintegration
IntegralCompProd
Invariance
MeasurableIntegral
WithDensity
Martingale
Basic
BorelCantelli
Centering
Convergence
OptionalSampling
OptionalStopping
Upcrossing
ProbabilityMassFunction
Basic
Binomial
Constructions
Integrals
Monad
Uniform
Process
Adapted
Filtration
HittingTime
Stopping
BorelCantelli
Cdf
CondCount
ConditionalExpectation
ConditionalProbability
Density
IdentDistrib
Integration
Moments
Notation
StrongLaw
Variance
RepresentationTheory
GroupCohomology
Basic
Hilbert90
LowDegree
Resolution
Action
Basic
Character
FdRep
Invariants
Maschke
Rep
RingTheory
Adjoin
Basic
FG
Field
PowerBasis
Tower
Coprime
Basic
Ideal
Lemmas
DedekindDomain
AdicValuation
Basic
Dvr
Factorization
FiniteAdeleRing
Ideal
IntegralClosure
PID
SInteger
SelmerGroup
Derivation
Basic
Lie
ToSquareZero
DiscreteValuationRing
Basic
TFAE
GradedAlgebra
Basic
HomogeneousIdeal
HomogeneousLocalization
Radical
Ideal
AssociatedPrime
Basic
Cotangent
IdempotentFG
LocalRing
MinimalPrime
Norm
Operations
Over
Prod
Quotient
QuotientOperations
Int
Basic
Localization
Away
AdjoinRoot
Basic
AsSubring
AtPrime
Basic
Cardinality
FractionRing
Ideal
Integer
Integral
InvSubmonoid
LocalizationLocalization
Module
NormTrace
NumDen
Submodule
MvPolynomial
Basic
Homogeneous
Ideal
NewtonIdentities
Symmetric
Tower
WeightedHomogeneous
NonUnitalSubring
Basic
NonUnitalSubsemiring
Basic
OreLocalization
Basic
OreSet
Polynomial
Cyclotomic
Basic
Eval
Expand
Roots
Eisenstein
Basic
IsIntegral
Hermite
Basic
Gaussian
Basic
Bernstein
Chebyshev
Content
Dickson
GaussLemma
IntegralNormalization
Nilpotent
Opposites
Pochhammer
Quotient
RationalRoot
ScaleRoots
Selmer
SeparableDegree
Tower
Vieta
PowerSeries
Basic
Derivative
WellKnown
RingHom
Finite
FiniteType
Integral
Surjective
RootsOfUnity
Basic
Complex
Minpoly
Subring
Basic
Pointwise
Subsemiring
Basic
Pointwise
Valuation
Basic
ExtendToLocalization
Integers
Integral
Quotient
RamificationGroup
ValuationRing
ValuationSubring
WittVector
Basic
Compare
Defs
DiscreteValuationRing
Domain
Frobenius
FrobeniusFractionField
Identities
InitTail
IsPoly
Isocrystal
MulCoeff
MulP
StructurePolynomial
Teichmuller
Truncated
Verschiebung
WittPolynomial
AdjoinRoot
AlgebraTower
Algebraic
AlgebraicIndependent
Artinian
Bezout
ChainOfDivisors
ClassGroup
Complex
Congruence
Discriminant
EisensteinCriterion
Etale
EuclideanDomain
Filtration
FinitePresentation
FiniteType
Finiteness
Fintype
Flat
FractionalIdeal
FreeCommRing
FreeRing
HahnSeries
Henselian
IntegralClosure
IntegralDomain
IntegrallyClosed
IsAdjoinRoot
IsTensorProduct
Jacobson
JacobsonIdeal
Kaehler
LaurentSeries
LocalProperties
MatrixAlgebra
Multiplicity
Nakayama
Nilpotent
Noetherian
NonZeroDivisors
Norm
Nullstellensatz
Perfection
PolynomialAlgebra
PowerBasis
Prime
PrincipalIdealDomain
QuotientNilpotent
QuotientNoetherian
ReesAlgebra
RingHomProperties
RingInvo
SimpleModule
TensorProduct
Trace
UniqueFactorizationDomain
ZMod
SetTheory
Cardinal
Basic
Cofinality
Continuum
CountableCover
Divisibility
Finite
Ordinal
SchroederBernstein
UnivLE
Game
Basic
Birthday
Domineering
Impartial
Nim
Ordinal
PGame
Short
State
Ordinal
Arithmetic
Basic
CantorNormalForm
Exponential
FixedPoint
NaturalOps
Notation
Principal
Topology
Surreal
Basic
Dyadic
ZFC
Basic
Ordinal
Lists
Tactic (file)
Attr
Core
Register
CancelDenoms (file)
Core
CategoryTheory
BicategoryCoherence
Coherence
Elementwise
Reassoc
Slice
Continuity (file)
Init
Explode (file)
Datatypes
Pretty
GCongr (file)
Core
ForwardAttr
Linarith (file)
Datatypes
Elimination
Frontend
Lemmas
Parsing
Preprocessing
Verification
Measurability (file)
Init
Monotonicity (file)
Attr
Basic
Lemmas
Nontriviality (file)
Core
NormNum (file)
Basic
BigOperators
Core
DivMod
Eq
GCD
Ineq
Inv
IsCoprime
LegendreSymbol
NatFib
NatSqrt
OfScientific
Pow
Prime
Result
Positivity (file)
Basic
Core
ReduceModChar (file)
Ext
Relation
Rfl
Symm
Trans
Ring (file)
Basic
PNat
RingNF
Sat
FromLRAT
Simps
Basic
NotationClass
Widget
Calc
CommDiag
Congrm
Conv
Gcongr
SelectInsertParamsClass
SelectPanelUtils
Abel
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Backtrack
Basic
ByContra
Cases
CasesM
Change
Choose
Classical
Clean
Clear!
ClearExcept
Clear_
Coe
Common
ComputeDegree
Congr!
Congrm
Constructor
Contrapose
Conv
Convert
Core
DefEqTransformations
DeriveFintype
DeriveToExpr
DeriveTraversable
Eqns
Existsi
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
Have
HaveI
HelpCmd
HigherOrder
Hint
InferParam
Inhabit
IntervalCases
IrreducibleDef
LibrarySearch
Lift
LiftLets
LinearCombination
Lint
MkIffOfInductiveProp
ModCases
MoveAdd
NoncommRing
NthRewrite
Observe
PPWithUniv
Peel
Polyrith
ProdAssoc
ProjectionNotation
Propose
ProxyType
PushNeg
Qify
RSuffices
Recall
Recover
Rename
RenameBVar
Replace
RewriteSearch
Rewrites
RunCmd
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SlimCheck
SolveByElim
SplitIfs
Spread
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TermCongr
ToAdditive
ToExpr
ToLevel
Trace
TryThis
TypeCheck
UnsetOption
Use
Variable
WLOG
Zify
Testing
SlimCheck
Functions
Gen
Sampleable
Testable
Topology
Algebra
Group
Basic
Compact
OpenMapping
TopologicalAbelianization
InfiniteSum
Basic
Module
Order
Real
Ring
Module
Alternating
Basic
Cardinality
CharacterSpace
Determinant
FiniteDimension
LinearPMap
LocallyConvex
Multilinear
Simple
Star
StrongTopology
WeakDual
Nonarchimedean
AdicTopology
Bases
Basic
Order
Archimedean
Compact
ExtendFrom
ExtrClosure
Field
Filter
Floor
Group
IntermediateValue
LeftRight
LeftRightLim
LiminfLimsup
MonotoneContinuity
MonotoneConvergence
ProjIcc
Rolle
T5
UpperLower
Ring
Basic
Ideal
Affine
Algebra
ConstMulAction
Constructions
ContinuousAffineMap
ContinuousMonoidHom
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Localization
Monoid
MulAction
OpenSubgroup
Polynomial
ProperConstSMul
Semigroup
Star
StarSubalgebra
UniformConvergence
UniformField
UniformFilterBasis
UniformGroup
UniformMulAction
UniformRing
Valuation
ValuedField
WithZeroTopology
Bornology
Basic
Constructions
Hom
Category
CompHaus
Basic
EffectiveEpi
Limits
Projective
LightProfinite
Basic
Profinite
AsLimit
Basic
CofilteredLimit
EffectiveEpi
Limits
Nobeling
Product
Projective
Stonean
Adjunctions
Basic
EffectiveEpi
Limits
TopCat
Limits
Basic
Cofiltered
Konig
Products
Pullbacks
Adjunctions
Basic
EpiMono
OpenNhds
Opens
Born
Compactum
Locale
TopCommRingCat
UniformSpace
Compactification
OnePoint
Compactness
Compact
LocallyCompact
Paracompact
SigmaCompact
Connected
Basic
LocallyConnected
PathConnected
TotallyDisconnected
ContinuousFunction
Algebra
Basic
Bounded
CocompactMap
Compact
Ideals
LocallyConstant
Ordered
Polynomial
Sigma
StoneWeierstrass
T0Sierpinski
Units
Weierstrass
ZeroAtInfty
EMetricSpace
Basic
Lipschitz
Paracompact
FiberBundle
Basic
Constructions
IsHomeomorphicTrivialBundle
Trivialization
Hom
Open
Homotopy
Basic
Contractible
Equiv
HSpaces
HomotopyGroup
Path
Product
Instances
AddCircle
Complex
Discrete
ENNReal
EReal
Int
Irrational
Matrix
NNReal
Nat
Rat
RatLemmas
Real
RealVectorSpace
Sign
TrivSqZeroExt
LocallyConstant
Algebra
Basic
MetricSpace
Algebra
Antilipschitz
Baire
Basic
Bounded
CantorScheme
CauSeqFilter
Cauchy
Closeds
Completion
Contracting
Dilation
DilationEquiv
Equicontinuity
Gluing
GromovHausdorff
GromovHausdorffRealized
HausdorffDimension
HausdorffDistance
Holder
Infsep
IsometricSMul
Isometry
Kuratowski
Lipschitz
MetricSeparated
PartitionOfUnity
PiNat
Polish
PseudoMetric
ShrinkingLemma
ThickenedIndicator
Metrizable
Basic
Uniformity
Urysohn
Order (file)
Category
AlexDisc
FrameAdjunction
Hom
Basic
Esakia
Basic
Bounded
Lattice
LowerUpperTopology
NhdsSet
Priestley
UpperLowerSetTopology
Separation (file)
NotNormal
Sets
Closeds
Compacts
Opens
Order
Sheaves
SheafCondition
EqualizerProducts
OpensLeCover
PairwiseIntersections
Sites
UniqueGluing
Abelian
Forget
Functors
Init
Limits
LocalPredicate
LocallySurjective
Operations
PUnit
Presheaf
PresheafOfFunctions
Sheaf
SheafOfFunctions
Sheafify
Skyscraper
Stalks
Spectral
Hom
UniformSpace
AbsoluteValue
AbstractCompletion
Basic
Cauchy
Compact
CompactConvergence
CompareReals
CompleteSeparated
Completion
Equicontinuity
Equiv
Matrix
Pi
Separation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
VectorBundle
Basic
Constructions
Hom
AlexandrovDiscrete
Bases
Basic
Clopen
CompactOpen
CompletelyRegular
Constructions
ContinuousOn
CountableSeparatingOn
Covering
DenseEmbedding
DiscreteQuotient
DiscreteSubset
ExtendFrom
ExtremallyDisconnected
Filter
GDelta
Gluing
Homeomorph
IndicatorConstPointwise
Inseparable
Irreducible
IsLocallyHomeomorph
List
LocalAtTarget
LocalExtr
LocalHomeomorph
LocallyFinite
Maps
NhdsSet
NoetherianSpace
OmegaCompletePartialOrder
Partial
PartitionOfUnity
Perfect
ProperMap
QuasiSeparated
Semicontinuous
SeparatedMap
Sequences
ShrinkingLemma
Sober
Specialization
StoneCech
Support
Tactic
TietzeExtension
UnitInterval
UrysohnsBounded
UrysohnsLemma
Util
AddRelatedDecl
AssertExists
AssertNoSorry
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
Export
Imports
IncludeStr
LongNames
MemoFix
Qq
SleepHeartbeats
Superscript
Syntax
SynthesizeUsing
Tactic
TermBeta
Time
WhatsNew
WithWeakNamespace
ProofWidgets (file)
Component
Panel
Basic
GoalTypePanel
SelectionPanel
Basic
HtmlDisplay
InteractiveSvg
MakeEditLink
OfRpcMethod
PenroseDiagram
Recharts
Data
Html
Svg
Presentation
Expr
Compat
Qq (file)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
SortLocalDecls
Typ
Std (file)
Classes
BEq
Cast
Dvd
LawfulMonad
Order
RatCast
SetNotation
CodeAction (file)
Attr
Basic
Deprecated
Misc
Control
ForInStep (file)
Basic
Lemmas
Lemmas
Data
Array
Init
Basic
Lemmas
Basic
Lemmas
Match
Merge
BinomialHeap (file)
Basic
Lemmas
BitVec (file)
Basic
Fin
Init
Lemmas
Basic
Lemmas
HashMap (file)
Basic
Lemmas
WF
Int
Basic
DivMod
Lemmas
List
Init
Attach
Lemmas
Basic
Count
Lemmas
Pairwise
MLList
Basic
Heartbeats
Nat
Init
Lemmas
Basic
Gcd
Lemmas
Option
Init
Lemmas
Basic
Lemmas
Prod
Lex
RBMap (file)
Alter
Basic
Lemmas
WF
Range
Lemmas
Rat (file)
Basic
Lemmas
String (file)
Basic
Lemmas
Sum (file)
Basic
Lemmas
AssocList
Bool
Char
DList
Json
Ord
PairingHeap
Lean
Elab
Tactic
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
Simp
UnusedNames
Util
EnvSearch
Path
AttributeExtra
Command
CoreM
Delaborator
Expr
Float
Format
HashMap
HashSet
InfoTree
Json
LocalContext
MonadBacktrack
Name
NameMapAttribute
Parser
PersistentHashMap
PersistentHashSet
Position
Tactic
TagAttribute
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Ext (file)
Attr
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
NormCast (file)
Ext
Lemmas
Relation
Rfl
Symm
Alias
Basic
ByCases
Case
Change
CoeExt
Congr
Exact
GuardExpr
GuardMsgs
HaveI
Instances
LabelAttr
LeftRight
NoMatch
OpenPrivate
PermuteGoals
PrintDependents
PrintPrefix
RCases
Replace
RunCmd
SeqFocus
ShowTerm
SimpTrace
Simpa
SqueezeScope
TryThis
Unreachable
Where
Test
Internal
DummyLabelAttr
Util
Cache
ExtendedBinder
LibraryNote
Pickle
ProofWanted
TermUnsafe
Logic
WF
docs (file)
Conv
Guide
Introduction

Color scheme