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
RuleExpr
Saturate
Tactic
Index (file)
Basic
Options (file)
Internal
Public
Rule (file)
Basic
Name
RuleSet (file)
Filter
Member
Name
RuleTac (file)
Forward (file)
Basic
Apply
Basic
Cases
ElabRuleTerm
Preprocess
Tactic
Script
CtorNames
GoalWithMVars
OptimizeSyntax
SScript
ScriptM
SpecificTactics
Step
StructureDynamic
StructureStatic
Tactic
TacticState
UScript
UScriptToSScript
Util
Search
Expansion (file)
Basic
Norm
Simp
Queue (file)
Class
ExpandSafePrefix
Main
RuleSelection
SearchM
Stats
Basic
Extension
Report
Tree (file)
AddRapp
Check
Data
ExtractProof
ExtractScript
Free
RunMetaM
State
Tracing
Traversal
TreeM
UnsafeQueue
Util
Tactic (file)
Ext
Unfold
Basic
EqualUpToIds
UnionFind
UnorderedArraySet
Check
Constants
ElabM
Exception
Main
Nanos
Percent
RulePattern
Saturate
Tracing
Batteries (file)
Classes
BEq
Cast
Order
RatCast
SatisfiesM
CodeAction (file)
Attr
Basic
Deprecated
Misc
Control
ForInStep (file)
Basic
Lemmas
Nondet
Basic
Lemmas
Data
Array (file)
Init
Lemmas
Basic
Lemmas
Match
Merge
Monadic
BinomialHeap (file)
Basic
Lemmas
BitVec (file)
Lemmas
Fin (file)
Basic
Lemmas
HashMap (file)
Basic
Lemmas
WF
Int (file)
DivMod
Lemmas
Order
List (file)
Init
Attach
Lemmas
Basic
Count
EraseIdx
Lemmas
Pairwise
Perm
MLList (file)
Basic
Heartbeats
IO
Nat (file)
Basic
Gcd
Lemmas
Option (file)
Lemmas
RBMap (file)
Alter
Basic
Depth
Lemmas
WF
Range (file)
Lemmas
Rat (file)
Basic
Lemmas
String (file)
Basic
Lemmas
Matcher
Sum (file)
Basic
Lemmas
UnionFind (file)
Basic
Lemmas
AssocList
BinaryHeap
Bool
ByteArray
Char
DList
LazyList
PairingHeap
Thunk
UInt
Lean
IO
Process
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
Simp
UnusedNames
System
IO
Util
EnvSearch
Path
AttributeExtra
Delaborator
Except
Expr
Float
HashMap
HashSet
Json
MonadBacktrack
Name
NameMap
NameMapAttribute
PersistentHashMap
PersistentHashSet
Position
SMap
Syntax
TagAttribute
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
Alias
Basic
Case
Classical
Congr
Exact
Init
Instances
NoMatch
OpenPrivate
PermuteGoals
PrintDependents
PrintPrefix
SeqFocus
ShowUnused
SqueezeScope
Unreachable
Where
Test
Internal
DummyLabelAttr
Util
Cache
CheckTactic
ExtendedBinder
LibraryNote
Pickle
ProofWanted
Logic
StdDeprecations
WF
ImportGraph
Imports
RequiredModules
Init (file)
Control (file)
Lawful (file)
Basic
Instances
Basic
EState
Except
ExceptCps
Id
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Subarray (file)
Split
Basic
BasicAux
BinSearch
DecidableEq
InsertionSort
Lemmas
Mem
QSort
BitVec (file)
Basic
Bitblast
Folds
Lemmas
ByteArray (file)
Basic
Char (file)
Basic
Lemmas
Fin (file)
Basic
Fold
Iterate
Lemmas
Log2
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Int (file)
Bitwise (file)
Lemmas
Basic
DivMod
DivModLemmas
Gcd
Lemmas
Order
Pow
List (file)
Basic
BasicAux
Control
Impl
Lemmas
TakeDrop
Nat (file)
Bitwise (file)
Basic
Lemmas
Basic
Compare
Control
Div
Dvd
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Power2
SOM
Simproc
Option (file)
Basic
BasicAux
Instances
Lemmas
String (file)
Basic
Extra
Lemmas
ToString (file)
Basic
Macro
UInt (file)
Basic
Lemmas
Log2
AC
Basic
Bool
Cast
Channel
Float
Hashable
OfScientific
Ord
Prod
Queue
Random
Range
Repr
Stream
Sum
Grind (file)
Cases
Lemmas
Norm
Tactics
Omega (file)
Coeffs
Constraint
Int
IntList
LinearCombo
Logic
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
BinderPredicates
ByCases
Classical
Coe
Conv
Core
Dynamic
Ext
GetElem
Guard
Hints
MacroTrace
Meta
MetaTypes
Notation
NotationExtra
Prelude
PropLemmas
RCases
ShareCommon
SimpLemmas
Simproc
SizeOf
SizeOfLemmas
Tactics
TacticsExtra
Util
WF
WFTactics
Lake (file)
Build (file)
Actions
Basic
Common
Data
Executable
Facets
Fetch
Imports
Index
Info
Job
Key
Library
Module
Package
Run
Store
Targets
Topological
Trace
CLI
Actions
Build
Error
Config (file)
Context
Defaults
Dependency
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InstallPath
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Module
Monad
Opaque
Package
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
AttributesCore
Config
DeclUtil
Extensions
Meta
Package
Require
Script
Targets
Load
Config
Toml (file)
Data
DateTime
Dict
Value
Elab (file)
Expression
Value
Grammar
Load
ParserUtil
Util
Binder
Casing
Compare
Cycle
DRBMap
EStateT
EquipT
Error
Exit
Family
FilePath
Git
IO
JsonObject
Lift
List
Lock
Log
Message
Name
NativeLib
Opaque
OrdHashSet
OrderedTagAttribute
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
Elab
FromToJson
Parser
Printer
Stream
Lsp (file)
Basic
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Workspace
Xml (file)
Basic
Parser
Array
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
GuessLex
Ite
Main
PackMutual
Preprocess
Rel
TerminationArgument
TerminationHint
Basic
Eqns
Main
MkInhabitant
Quotation (file)
Precheck
Util
Tactic (file)
Conv (file)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Omega (file)
Core
Frontend
MinNatAbs
OmegaM
Basic
BuiltinTactic
Cache
Calc
Change
Config
Congr
Delta
ElabTerm
Ext
FalseOrByContra
Generalize
Guard
Induction
Injection
LibrarySearch
Location
Match
Meta
NormCast
RCases
Repeat
Rewrite
Rewrites
Rfl
ShowTerm
Simp
SimpTrace
Simpa
Simproc
SolveByElim
Split
Symm
Unfold
App
Arg
Attributes
AutoBound
AuxDef
BinderPredicates
Binders
BindersUtil
BuiltinCommand
BuiltinNotation
BuiltinTerm
Calc
CheckTactic
Command
ComputedFields
Config
DeclModifiers
DeclNameGen
DeclUtil
Declaration
DeclarationRange
DefView
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
GuardMsgs
Import
Inductive
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
MatchExpr
Mixfix
MutualDef
Notation
Open
ParseImportsFast
PatternVar
Print
RecAppSyntax
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Term
Util
Language
Basic
Lean
Linter (file)
Basic
Builtin
Deprecated
MissingDocs
UnusedVariables
Util
Meta (file)
ArgsPacker (file)
Basic
Match (file)
MatcherApp
Basic
Transform
Basic
CaseArraySizes
CaseValues
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
Tactic (file)
AC (file)
Main
Grind (file)
Attr
Cases
Core
Injection
Preprocessor
RevertAll
Types
Util
LinearArith (file)
Nat (file)
Basic
Simp
Solver
Basic
Main
Simp
Solver
Simp (file)
BuiltinSimprocs (file)
BitVec
Char
Core
Fin
Int
Nat
String
UInt
Util
Attr
Diagnostics
Main
RegisterCommand
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Simproc
Types
Acyclic
Apply
Assert
Assumption
AuxLemma
Backtrack
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
FVarSubst
FunInd
Generalize
IndependentOf
Induction
Injection
Intro
LibrarySearch
NormCast
Refl
Rename
Repeat
Replace
Revert
Rewrite
Rewrites
Rfl
SolveByElim
Split
SplitIf
Subst
Symm
TryThis
Unfold
UnifyEq
Util
ACLt
AbstractMVars
AbstractNestedProofs
AppBuilder
Basic
Canonicalizer
Check
CheckTactic
Closure
Coe
CoeAttr
CollectFVars
CollectMVars
CompletionName
CongrTheorems
Constructions
CtorRecognizer
DecLevel
Diagnostics
DiscrTree
DiscrTreeTypes
Eqns
Eval
ExprDefEq
ExprLens
ExprTraverse
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetUnfoldableConst
GlobalInstances
IndPredBelow
Inductive
InferType
Injective
Instances
Iterator
KAbstract
KExprMap
LazyDiscrTree
LevelDefEq
LitValues
MatchUtil
NatInstTesters
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)
Attributes
Basic
Builtins
FieldNotation
Options
SubExpr
TopDownAnalyze
Basic
Formatter
Parenthesizer
Server (file)
CodeActions (file)
Attr
Basic
Provider
FileWorker (file)
RequestHandling
SetupFile
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
AsyncList
Completion
CompletionItemData
FileSource
GoTo
ImportCompletion
InfoUtils
References
Requests
Snapshots
Utils
Watchdog
Util (file)
CollectFVars
CollectLevelParams
CollectMVars
Diff
FileSetupInfo
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
Heartbeats
InstantiateLevelParams
LakePath
LeanOptions
MonadBacktrack
MonadCache
OccursCheck
PPExt
Path
Paths
Profile
Profiler
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SCC
ShareCommon
Sorry
TestExtern
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
DocString
Environment
Eval
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LabelAttribute
LazyInitExtension
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
ProjFns
ReducibilityAttrs
ReservedNameAction
ResolveName
Runtime
ScopedEnvExtension
Structure
SubExpr
Syntax
ToExpr
Mathlib
Algebra
Algebra
Subalgebra
Basic
Operations
Prod
Tower
Unitization
Basic
Bilinear
Defs
Equiv
Hom
NonUnitalHom
NonUnitalSubalgebra
Operations
Opposite
Pi
Prod
RestrictScalars
Spectrum
Tower
Unitization
BigOperators
Group
Finset
List
Multiset
GroupWithZero
Finset
Ring (file)
List
Multiset
Associated
Fin
Finprod
Finsupp
Intervals
Module
NatAntidiagonal
Option
Pi
RingEquiv
WithTop
CharP
Algebra
Basic
Defs
ExpChar
Invertible
Reduced
Two
CharZero
Defs
Lemmas
Quotient
DirectSum
Basic
Decomposition
Finsupp
Module
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Instances
Field
Basic
Defs
Equiv
IsField
Opposite
Rat
Subfield
FreeMonoid
Basic
GCDMonoid
Basic
Finset
Multiset
Nat
Group
Action
Defs
Commute
Basic
Defs
Hom
Units
Equiv
Basic
TypeTags
Hom
Basic
CompTypeclasses
Defs
End
Instances
Invertible
Basic
Defs
Pi
Basic
Lemmas
Semiconj
Basic
Defs
Units
Subgroup
Actions
Basic
Finite
MulOpposite
Pointwise
ZPowers
Submonoid
Basic
Membership
MulOpposite
Operations
Pointwise
Subsemigroup
Basic
Membership
Operations
Units (file)
Equiv
Hom
WithOne
Defs
AddChar
Aut
Basic
Center
Centralizer
Commutator
Conj
ConjFinite
Defs
Embedding
Even
Fin
FiniteSupport
Indicator
InjSurj
Int
Nat
Opposite
Prod
Support
TypeTags
ULift
UniqueProds
GroupPower
IterateHom
GroupWithZero
Units
Basic
Equiv
Lemmas
Basic
Commute
Defs
Divisibility
Hom
Indicator
InjSurj
Invertible
NeZero
NonZeroDivisors
Pi
Prod
Semiconj
ULift
WithZero
Module
LinearMap
Basic
End
Prod
Star
Submodule
Basic
Bilinear
EqLocus
Equiv
IterateMapComap
Ker
Lattice
LinearMap
Map
Pointwise
Range
RestrictScalars
Basic
BigOperators
Defs
Equiv
Hom
MinimalAxioms
Opposites
Pi
Prod
Torsion
ULift
MonoidAlgebra
Basic
Degree
Division
NoZeroDivisors
Support
MvPolynomial
Basic
CommRing
Degrees
Derivation
Equiv
PDeriv
Rename
Supported
Variables
Order
Antidiag
Prod
BigOperators
Group
Finset
List
Multiset
Ring
Finset
List
Multiset
CauSeq
Basic
BigOperators
Completion
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Power
Rat
Group
Abs
Action
Basic
Defs
Indicator
InjSurj
Instances
Int
Lattice
MinMax
Nat
OrderIso
PosPart
Prod
Synonym
TypeTags
Units
GroupWithZero
Canonical
Synonym
Unbundled
Hom
Basic
Monoid
Ring
Interval
Set
Group
Instances
Monoid
Finset
Module
Algebra
Defs
OrderedSMul
Pointwise
Synonym
Monoid
Canonical
Defs
Unbundled
Basic
Defs
MinMax
Pow
Basic
Defs
NatCast
OrderDual
Prod
Submonoid
TypeTags
Units
WithTop
Nonneg
Field
Floor
Ring
Positive
Ring
Ring
Abs
Basic
Canonical
Cast
Defs
Finset
InjSurj
Int
Nat
Pow
Rat
Synonym
WithTop
Sub
Canonical
Defs
WithTop
AbsoluteValue
Archimedean
Floor
Invertible
Kleene
Monovary
Pi
ToIntervalMod
ZeroLEOne
Polynomial
Degree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
BigOperators
CancelLeads
Coeff
Derivative
Div
EraseLead
Eval
FieldDivision
Induction
Inductions
Lifts
Monic
Monomial
Reverse
RingDivision
Roots
Splits
Regular
Basic
Pow
SMul
Ring
Action
Basic
Group
Subobjects
Divisibility
Basic
Hom
Basic
Defs
Subring
Basic
Units
Subsemiring
Basic
AddAut
Aut
Basic
Center
Centralizer
Commute
CompTypeclasses
Defs
Equiv
Fin
Idempotents
InjSurj
Int
Invertible
Nat
NegOnePow
Opposite
Parity
Pi
Prod
Rat
Regular
Semiconj
ULift
Units
Squarefree
Basic
Star
Basic
BigOperators
Center
Module
NonUnitalSubalgebra
Order
Pi
Pointwise
Prod
Rat
SelfAdjoint
StarAlgHom
StarRingHom
Subalgebra
Unitary
AddTorsor
Associated
Bounds
FreeAlgebra
GeomSum
ModEq
NeZero
Opposites
PUnitInstances
Periodic
QuadraticDiscriminant
Quotient
SMulWithZero
Analysis
Analytic
Basic
CPolynomial
Asymptotics
AsymptoticEquivalent
Asymptotics
Theta
BoxIntegral
Box
Basic
SubboxInduction
Partition
Additive
Basic
Filter
Measure
Split
SubboxInduction
Tagged
Basic
DivergenceTheorem
Integrability
Calculus
Conformal
NormedSpace
ContDiff
Basic
Bounds
Defs
RCLike
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
Mul
Pow
Prod
Shift
Slope
Support
ZPow
FDeriv
Add
Analytic
Basic
Bilinear
Comp
Equiv
Extend
Linear
Measurable
Mul
Prod
RestrictScalars
InverseFunctionTheorem
ApproximatesLinearOn
Deriv
FDeriv
IteratedDeriv
Defs
Lemmas
LineDeriv
Basic
LocalExtr
Basic
Rolle
DiffContOnCl
Dslope
FormalMultilinearSeries
MeanValue
ParametricIntegral
SmoothSeries
TangentCone
UniformLimitsDeriv
Complex
UpperHalfPlane
Basic
Asymptotics
Basic
CauchyIntegral
Circle
Conformal
Isometry
ReImTopology
RealDeriv
Convex
Cone
Basic
Extension
SpecificFunctions
Basic
Deriv
Basic
Between
Combination
Complex
Deriv
Function
Gauge
Hull
Integral
Jensen
Mul
Normed
Segment
Slope
Star
Strict
StrictConvexSpace
Topology
Uniform
Distribution
SchwartzSpace
Fourier
AddCircle
FourierTransform
PoissonSummation
InnerProductSpace
Basic
GramSchmidtOrtho
Orientation
Orthogonal
PiL2
Projection
Symmetric
l2Space
LocallyConvex
BalancedCoreHull
Basic
Bounded
Polar
WithSeminorms
Normed
Field
Basic
InfiniteSum
UnitBall
Group
AddCircle
AddTorsor
BallSphere
Basic
Bounded
Completion
Constructions
Hom
InfiniteSum
Int
Lemmas
Pointwise
Quotient
Rat
Seminorm
Submodule
Uniform
ZeroAtInfty
Order
Basic
Lattice
MulAction
NormedSpace
HahnBanach
Extension
SeparatingDual
Separation
Multilinear
Basic
Curry
OperatorNorm
Asymptotics
Basic
Bilinear
Completeness
Mul
NNNorm
NormedSpace
Prod
Star
Basic
AddTorsor
AffineIsometry
Banach
Basic
BoundedLinearMaps
Completion
ConformalLinearMap
ContinuousLinearMap
Dual
Exponential
Extend
FiniteDimension
FunctionSeries
IndicatorFunction
LinearIsometry
PiLp
Pointwise
RCLike
Ray
Real
RieszLemma
Span
Units
WithLp
lpSpace
RCLike
Basic
Lemmas
SpecialFunctions
Complex
Arg
Circle
Log
LogDeriv
Gamma
Basic
Gaussian
FourierTransform
GaussianIntegral
PoissonSummation
Log
Base
Basic
Deriv
Pow
Asymptotics
Complex
Continuity
Deriv
NNReal
Real
Trigonometric
Angle
Arctan
ArctanDeriv
Basic
Complex
ComplexDeriv
Deriv
Inverse
Bernstein
Exp
ExpDeriv
Exponential
ImproperIntegrals
Integrals
JapaneseBracket
NonIntegrable
PolarCoord
Sqrt
SpecificLimits
Basic
Normed
MeanInequalities
MeanInequalitiesPow
MellinTransform
PSeries
Seminorm
SumOverResidueClass
Combinatorics
Enumerative
Composition
Partition
Control
Monad
Basic
Traversable
Basic
Applicative
Basic
Bifunctor
EquivFunctor
Functor
ULift
Data
Array
Defs
Bool
Basic
Set
Complex
Abs
Basic
BigOperators
Cardinality
Exponential
FiniteDimensional
Module
Order
Countable
Basic
Defs
DFinsupp
Basic
Encodable
ENNReal
Basic
Inv
Operations
Real
ENat
Basic
Lattice
Fin
Tuple
Basic
Basic
VecNotation
Finite
Basic
Card
Defs
Set
Finset
Attr
Basic
Card
Fin
Fold
Image
Lattice
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
Piecewise
Pointwise
Powerset
Preimage
Prod
Sigma
Sort
Sum
Sym
Union
Update
Finsupp
Antidiagonal
Basic
Defs
Encodable
Fin
Fintype
Indicator
Multiset
Order
ToDFinsupp
Fintype
Basic
BigOperators
Card
CardEmbedding
Fin
Lattice
List
Option
Order
Parity
Perm
Pi
Powerset
Prod
Sigma
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Order
Lemmas
Units
Bitwise
CharZero
ConditionallyCompleteOrder
Defs
GCD
Interval
LeastGreatest
Lemmas
Log
ModEq
Sqrt
SuccPred
List
Basic
Chain
Count
Cycle
Dedup
Defs
Duplicate
Enum
FinRange
Forall2
GetD
Indexes
Infix
InsertNth
Join
Lattice
Lex
MinMax
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
ProdSigma
Range
Rotate
Sort
Sublists
Sym
TFAE
Zip
Matrix
Basic
Basis
Block
DMatrix
Invertible
Notation
RowCol
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
NatAntidiagonal
Nodup
Pi
Powerset
Range
Sections
Sort
Sum
Sym
NNRat
Defs
NNReal
Basic
Star
Nat
Cast
Basic
Commute
Defs
Field
NeZero
Order
Prod
WithTop
Choose
Basic
Cast
Multinomial
Sum
Factorial
Basic
BigOperators
Cast
Factorization
Basic
GCD
Basic
BigOperators
Order
Lemmas
Bits
Bitwise
Count
Defs
Digits
Factors
Lattice
Log
MaxPowDiv
ModEq
Multiplicity
Pairing
PartENat
Periodic
Prime
PrimeFin
Set
Size
SuccPred
Totient
WithBot
Option
Basic
Defs
NAry
PNat
Basic
Defs
Equiv
Prod
Basic
Lex
PProd
TProd
Rat
Cast
CharZero
Defs
Lemmas
Order
BigOperators
Defs
Denumerable
Encodable
Floor
Init
Lemmas
Real
Archimedean
Basic
Cardinality
ConjExponents
EReal
Pointwise
Sqrt
Star
Set
Pairwise
Basic
Lattice
Pointwise
Basic
BigOperators
Finite
Interval
ListOfFn
SMul
Accumulate
Basic
BoolIndicator
Countable
Defs
Finite
Function
Functor
Image
Lattice
List
MemPartition
NAry
Prod
Semiring
Sigma
Subsingleton
UnionLift
SetLike
Basic
Setoid
Basic
Sigma
Basic
Lex
String
Defs
Sum
Basic
Order
Sym
Sym2 (file)
Init
Basic
Tree
Basic
Vector
Basic
Defs
W
Basic
Cardinal
ZMod
Basic
Defs
IntUnitsPower
Quotient
Bracket
Part
Quot
Rel
SProd
Sign
Subtype
ULift
Dynamics
Ergodic
MeasurePreserving
FixedPoints
Basic
Minimal
PeriodicPts
FieldTheory
Finiteness
GroupTheory
Congruence
Basic
GroupAction
DomAct
Basic
SubMulAction (file)
Pointwise
Basic
BigOperators
ConjAct
Defs
Group
Hom
Opposite
Pi
Pointwise
Prod
Quotient
Ring
Units
Perm
Cycle
Basic
Factors
Type
Basic
Closure
Fin
Finite
List
Option
Sign
Support
SpecificGroups
Cyclic
Subgroup
Center
Centralizer
Simple
Submonoid
Center
Centralizer
Subsemigroup
Center
Centralizer
Archimedean
Commutator
Coset
Divisible
Exponent
Finiteness
Index
MonoidLocalization
NoncommPiCoprod
OrderOfElement
PGroup
QuotientGroup
Torsion
Init
Algebra
Classes
Control
Combinators
Data
Bool
Lemmas
Fin
Basic
Int
Basic
Order
List
Basic
Instances
Lemmas
Nat
Basic
Lemmas
Notation
Ordering
Basic
Sigma
Basic
Lex
Prod
Quot
Order
Defs
LinearOrder
Align
Classical
Core
Function
Logic
Quot
Set
ZeroOne
Lean
Elab
Tactic
Basic
Term
Expr
Basic
ExtraRecognizers
ReplaceRec
Meta (file)
Basic
CongrTheorems
Simp
PrettyPrinter
Delaborator
EnvExtension
Name
LinearAlgebra
AffineSpace
AffineEquiv
AffineMap
AffineSubspace
Basic
Basis
Combination
FiniteDimensional
Independent
Midpoint
Ordered
Restrict
Slope
Alternating
Basic
Basis (file)
VectorSpace
Dimension
Basic
Constructions
DivisionRing
Finite
Finrank
Free
FreeAndStrongRankCondition
LinearMap
RankNullity
StrongRankCondition
DirectSum
Finsupp
TensorProduct
FreeModule
Finite
Basic
Matrix
Basic
StrongRankCondition
Matrix
Determinant
Basic
Adjugate
Basis
Block
Diagonal
GeneralLinearGroup
MvPolynomial
NonsingularInverse
Polynomial
Reindex
SpecialLinearGroup
ToLin
Trace
Transvection
Multilinear
Basic
Basis
TensorProduct
Basic
Basis
Tower
BilinearMap
DFinsupp
Determinant
Dual
FiniteDimensional
Finsupp
FinsuppVectorSpace
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
LinearIndependent
LinearPMap
Orientation
Pi
Prod
Projection
Quotient
Ray
SesquilinearForm
Span
StdBasis
UnitaryGroup
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Basic
Defs
Embedding
Fin
Fintype
Functor
List
Nat
Option
PartialEquiv
Set
TransferInstance
Function
Basic
CompTypeclasses
Conjugate
Iterate
Nontrivial
Basic
Defs
Small
Basic
Defs
Set
Basic
Denumerable
IsEmpty
Nonempty
Pairwise
Relation
Relator
Unique
Mathport
Attributes
Notation
Rename
MeasureTheory
Constructions
BorelSpace
Basic
Complex
ContinuousLinearMap
Metric
Metrizable
Order
Real
Prod
Basic
Integral
EventuallyMeasurable
Pi
Polish
Covering
Besicovitch
BesicovitchVectorSpace
Differentiation
VitaliFamily
Decomposition
Jordan
Lebesgue
RadonNikodym
SignedHahn
SignedLebesgue
Function
ConditionalExpectation
AEMeasurable
Basic
CondexpL1
CondexpL2
Unique
LpSeminorm
Basic
ChebyshevMarkov
CompareExp
TriangleInequality
Trim
SpecialFunctions
Basic
StronglyMeasurable
Basic
Inner
Lemmas
Lp
AEEqFun
AEEqOfIntegral
AEMeasurableOrder
AEMeasurableSequence
ContinuousMapDense
EssSup
Jacobian
L1Space
L2Space
LocallyIntegrable
LpOrder
LpSpace
SimpleFunc
SimpleFuncDense
SimpleFuncDenseLp
Group
Action
Arithmetic
FundamentalDomain
Integral
LIntegral
MeasurableEquiv
Measure
Pointwise
Prod
Integral
Asymptotics
Average
Bochner
CircleIntegral
DivergenceTheorem
DominatedConvergence
ExpDecay
FundThmCalculus
IntegrableOn
IntegralEqImproper
IntervalIntegral
Layercake
Lebesgue
Marginal
MeanInequalities
Periodic
Pi
SetIntegral
SetToL1
VitaliCaratheodory
MeasurableSpace
Basic
CountablyGenerated
Defs
Embedding
Instances
Measure
Haar
Basic
InnerProductSpace
NormedSpace
OfBasis
Quotient
Unique
Lebesgue
Basic
Complex
EqHaar
Integral
AEDisjoint
AEMeasurable
Complex
Content
Count
Dirac
Doubling
EverywherePos
GiryMonad
MeasureSpace
MeasureSpaceDef
MutuallySingular
NullMeasurable
OpenPos
Regular
Restrict
Stieltjes
Sub
Trim
Typeclasses
VectorMeasure
WithDensity
WithDensityVectorMeasure
Order
Lattice
OuterMeasure
AE
Basic
Caratheodory
Defs
Induced
OfFunction
Operations
PiSystem
NumberTheory
ModularForms
JacobiTheta
OneVariable
TwoVariable
Padics
PadicVal
Divisors
Order
Atoms (file)
Finite
Bounds
Basic
OrderIso
CompactlyGenerated
Basic
Intervals
ConditionallyCompleteLattice
Basic
Finset
Group
Filter
Archimedean
AtTopBot
Bases
Basic
Cofinite
CountableInter
CountableSeparatingOn
Curry
ENNReal
EventuallyConst
Extr
Germ
IndicatorFunction
Interval
Ker
Lift
ModEq
NAry
Pi
Pointwise
Prod
Ring
SmallSets
Subsingleton
Ultrafilter
Heyting
Basic
Hom
Basic
Bounded
CompleteLattice
Lattice
Order
Set
Interval
Finset
Basic
Defs
Fin
Nat
Set
Basic
Disjoint
Image
Infinite
Monotone
OrdConnected
OrdConnectedComponent
OrderEmbedding
OrderIso
Pi
ProjIcc
UnorderedInterval
WithBotTop
Multiset
Monotone
Basic
Monovary
Odd
Union
RelIso
Basic
Set
SuccPred
Basic
CompleteLinearOrder
Limit
Relation
UpperLower
Basic
Antichain
Antisymmetrization
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
Compare
CompleteBooleanAlgebra
CompleteLattice
CompleteLatticeIntervals
Copy
Cover
Directed
Disjoint
Disjointed
Fin
FixedPoints
GaloisConnection
InitialSeg
Iterate
JordanHolder
Lattice
LatticeIntervals
LiminfLimsup
Max
MinMax
Minimal
ModularLattice
Nat
Notation
OmegaCompletePartialOrder
OrderIsoNat
PartialSups
PiLex
PropInstances
RelClasses
RelSeries
SetNotation
SupClosed
SupIndep
SymmDiff
Synonym
ULift
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
Probability
Distributions
Uniform
Independence
Basic
Kernel
Kernel
Basic
ProbabilityMassFunction
Basic
Constructions
Integrals
Monad
ConditionalProbability
Density
Notation
RingTheory
Adjoin
Basic
FG
Tower
Congruence
Basic
Coprime
Basic
Ideal
Lemmas
Derivation
Basic
Ideal
Basic
Colon
IsPrimary
LocalRing
Maps
Operations
Quotient
QuotientOperations
Int
Basic
Localization
Basic
FractionRing
MvPolynomial
Symmetric
Nilpotent
Basic
Defs
Lemmas
NonUnitalSubring
Basic
NonUnitalSubsemiring
Basic
OreLocalization
Basic
OreSet
Polynomial
Basic
Bernstein
Content
Pochhammer
Quotient
Vieta
RootsOfUnity
Basic
TensorProduct
Basic
AlgebraTower
EuclideanDomain
FiniteType
Finiteness
IntegralDomain
JacobsonIdeal
Multiplicity
Noetherian
OrzechProperty
PrincipalIdealDomain
SimpleModule
UniqueFactorizationDomain
ZMod
SetTheory
Cardinal
Basic
Cofinality
Continuum
ENat
Finite
Ordinal
PartENat
SchroederBernstein
Subfield
ToNat
Ordinal
Arithmetic
Basic
Exponential
FixedPoint
Principal
Tactic
Attr
Core
Register
CC (file)
Addition
Datatypes
Lemmas
CancelDenoms
Core
Continuity (file)
Init
FunProp (file)
Attr
Core
Decl
Elab
FunctionData
Mor
RefinedDiscrTree
StateList
Theorems
ToBatteries
Types
GCongr (file)
Core
ForwardAttr
Linarith (file)
Oracle
SimplexAlgorithm (file)
Datatypes
Gauss
PositiveVector
SimplexAlgorithm
Datatypes
Frontend
Lemmas
Parsing
Preprocessing
Verification
Linter (file)
GlobalAttributeIn
HashCommandLinter
Lint
OldObtain
Style
UnusedTactic
Measurability (file)
Init
Monotonicity (file)
Attr
Basic
Lemmas
Nontriviality (file)
Core
NormNum (file)
Basic
Core
DivMod
Eq
GCD
Ineq
Inv
OfScientific
Pow
Result
Positivity (file)
Basic
Core
Relation
Rfl
Symm
Trans
Ring (file)
Basic
PNat
RingNF
Simps
Basic
NotationClass
Widget
Calc
Congrm
Conv
SelectInsertParamsClass
SelectPanelUtils
Abel
AdaptationNote
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Basic
ByContra
Cases
CasesM
Check
Choose
ClearExcept
ClearExclamation
Clear_
Coe
Common
ComputeDegree
Congr!
Congrm
Constructor
Contrapose
Conv
Convert
Core
DefEqTransformations
DeprecateMe
DeriveToExpr
Eqns
Existsi
ExtendDoc
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
Generalize
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
HaveI
HelpCmd
HigherOrder
Hint
InferParam
Inhabit
IntervalCases
IrreducibleDef
Lemma
Lift
LinearCombination
MkIffOfInductiveProp
MoveAdd
NoncommRing
NthRewrite
Observe
PPWithUniv
Peel
ProjectionNotation
Propose
PushNeg
RSuffices
Recover
Rename
RenameBVar
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SplitIfs
Spread
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TermCongr
ToAdditive
ToExpr
ToLevel
Trace
TryThis
TypeCheck
TypeStar
UnsetOption
Use
Variable
WLOG
Zify
Topology
Algebra
Group
Basic
Compact
InfiniteSum
Basic
Constructions
Defs
Group
Module
NatInt
Order
Real
Ring
Module
Multilinear
Basic
Bounded
Topology
Basic
Determinant
FiniteDimension
LocallyConvex
Simple
Star
StrongTopology
UniformConvergence
WeakDual
Order
Archimedean
Compact
Field
Floor
Group
LiminfLimsup
Rolle
Ring
Basic
Ideal
Affine
Algebra
ConstMulAction
Constructions
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Monoid
MulAction
Polynomial
Star
StarSubalgebra
UniformConvergence
UniformFilterBasis
UniformGroup
UniformMulAction
UniformRing
Baire
CompleteMetrizable
Lemmas
Bornology
Absorbs
Basic
BoundedOperation
Constructions
Hom
Compactness
Compact
Lindelof
LocallyCompact
SigmaCompact
Connected
Basic
LocallyConnected
PathConnected
TotallyDisconnected
ContinuousFunction
Algebra
Basic
Bounded
CocompactMap
Compact
ContinuousMapZero
Ordered
Polynomial
StoneWeierstrass
Weierstrass
ZeroAtInfty
Defs
Basic
Filter
Induced
Sequences
EMetricSpace
Basic
Lipschitz
FiberBundle
IsHomeomorphicTrivialBundle
Instances
AddCircle
Discrete
ENNReal
EReal
Int
Matrix
NNReal
Nat
Rat
Real
RealVectorSpace
Sign
MetricSpace
Pseudo
Constructions
Defs
Lemmas
Algebra
Antilipschitz
Basic
Bounded
CantorScheme
CauSeqFilter
Cauchy
Completion
Dilation
DilationEquiv
Equicontinuity
Gluing
HausdorffDistance
IsometricSMul
Isometry
Lipschitz
Perfect
PiNat
Polish
ProperSpace
ThickenedIndicator
Thickening
Metrizable
Basic
Uniformity
Urysohn
Order (file)
Basic
Bornology
DenselyOrdered
ExtendFrom
IntermediateValue
IsLUB
Lattice
LeftRight
LeftRightLim
LeftRightNhds
LocalExtr
Monotone
MonotoneContinuity
MonotoneConvergence
OrderClosed
ProjIcc
T5
Sets
Closeds
Compacts
Opens
UniformSpace
AbstractCompletion
Basic
Cauchy
Compact
CompactConvergence
CompleteSeparated
Completion
Equicontinuity
Equiv
Pi
Separation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
Bases
Basic
Clopen
CompactOpen
Constructions
ContinuousOn
CountableSeparatingOn
DenseEmbedding
DiscreteSubset
ExtendFrom
Filter
GDelta
Homeomorph
IndicatorConstPointwise
Inseparable
Irreducible
IsLocalHomeomorph
LocallyFinite
Maps
NhdsSet
NoetherianSpace
PartialHomeomorph
Perfect
ProperMap
QuasiSeparated
RestrictGenTopology
Semicontinuous
SeparatedMap
Separation
Sequences
StoneCech
Support
UnitInterval
UrysohnsLemma
Util
AssertExists
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
MemoFix
Qq
SynthesizeUsing
Tactic
WhatsNew
WithWeakNamespace
ProofWidgets (file)
Component
Panel
Basic
GoalTypePanel
SelectionPanel
Basic
FilterDetails
HtmlDisplay
InteractiveSvg
MakeEditLink
OfRpcMethod
PenroseDiagram
Recharts
Data
Html
Svg
Presentation
Expr
Cancellable
Compat
Util
Qq (file)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
SortLocalDecls
Typ
SampCert (file)
DifferentialPrivacy
Pure
Mechanism
Basic
Code
Properties
AdaptiveComposition
Composition
Const
DP
Postprocessing
System
Queries
BoundedMean
Basic
Code
Properties
BoundedSum
Basic
Code
Properties
Count
Basic
Code
Properties
Histogram
Basic
Code
Properties
HistogramMean
Code
Properties
ZeroConcentrated
Mechanism
Basic
Code
Properties
AdaptiveComposition
Composition
ConcentratedBound
Const
DP
Postprocessing
System
Abstract
Neighbours
RenyiDivergence
Sensitivity
Foundations
Auto
Basic
Monad
UniformP2
Until
While
Samplers
Bernoulli
Basic
Code
Properties
BernoulliNegativeExponential
Basic
Code
Properties
Gaussian
Code
Properties
GaussianGen
Basic
Code
Properties
Geometric
Basic
Code
Properties
Laplace
Basic
Code
Properties
LaplaceGen
Basic
Code
Properties
Uniform
Basic
Code
Properties
Util
Gaussian
DiscreteGaussian
GaussBound
GaussConvergence
GaussPeriodicity
Log
Shift
Util
UtilMathlib
SLang

Color scheme