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
RuleApplicationWithMVarInfo
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
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
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
Util
Async
Binder
Casing
Compare
Cycle
DRBMap
EStateT
EquipT
Error
EvalTerm
Exit
Family
Git
Lift
List
Log
Name
NativeLib
Opaque
OptionIO
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
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
LeanAPAP (file)
FiniteField
Basic
HoelderLifting
Integer
HoelderLifting
Mathlib
Algebra
BigOperators
Basic
Expect
Order
Pi
Ring
DirectSum
Basic
Group
Basic
TypeTags
GroupPower
Basic
Hom
Order
Hom
Equiv
Basic
Group
GroupInstances
Module
Basic
Order
Ring
Canonical
LatticeGroup
SMul
Star
Basic
Order
Pi
SelfAdjoint
Support
Analysis
Complex
Basic
Circle
InnerProductSpace
PiL2
Normed
Field
Basic
Group
Basic
NormedSpace
PiLp
Ray
SpecialFunctions
Log
Basic
Pow
Real
MeanInequalities
MeanInequalitiesPow
Data
Complex
Basic
Exponential
Finset
Basic
Card
Image
NatAntidiagonal
Pointwise
Powerset
Fintype
Basic
Card
Lattice
Pi
FunLike
Basic
IsROrC
Basic
Nat
Cast
Field
Choose
Multinomial
Factorial
Basic
BigOperators
DoubleFactorial
Order
Basic
Parity
Pi
Algebra
Rat
Order
Real
Basic
ENNReal
NNReal
Sqrt
ZMod
Basic
GroupTheory
GroupAction
BigOperators
Submonoid
Basic
Operations
FiniteAbelian
OrderOfElement
LinearAlgebra
FiniteDimensional
Ray
Logic
Basic
NumberTheory
LegendreSymbol
AddChar
Basic
Duality
Order
ConditionallyCompleteLattice
Finset
Heyting
Basic
Partition
Finpartition
Disjoint
Tactic
Binop
Positivity
Physics
AlmostPeriodicity
DRC
Unbalancing
Prereqs
Convolution
Basic
Norm
Order
WithConv
Chang
Cut
DFT
Dissociation
Energy
Indicator
LpNorm
MarcinkiewiczZygmund
Misc
Multinomial
Rudin
SalemSpencer
Translate
Mathlib
Algebra
Algebra
Subalgebra
Basic
Pointwise
Tower
Basic
Bilinear
Equiv
Hom
Operations
Opposite
Pi
Prod
RestrictScalars
Tower
BigOperators
Multiset
Basic
Lemmas
Associated
Basic
Fin
Finprod
Finsupp
Intervals
NatAntidiagonal
Option
Order
Pi
Ring
RingEquiv
Category
GroupCat
Basic
Limits
Preadditive
ModuleCat
Abelian
Basic
Biproducts
EpiMono
Kernels
Limits
MonCat
Basic
Limits
CharP
Algebra
Basic
Invertible
Two
CharZero
Defs
Infinite
Lemmas
Quotient
DirectSum
Basic
Decomposition
Finsupp
Module
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Instances
Field
Basic
Defs
IsField
Opposite
FreeMonoid
Basic
GCDMonoid
Basic
Finset
IntegrallyClosed
Multiset
Group
Commute
Defs
Units
Semiconj
Defs
Units
WithOne
Defs
Basic
Commutator
Conj
ConjFinite
Defs
Ext
InjSurj
Opposite
OrderSynonym
Pi
Prod
TypeTags
ULift
Units
GroupPower
Basic
Lemmas
Order
Ring
GroupRingAction
Basic
Invariant
Subobjects
GroupWithZero
Units
Basic
Lemmas
Basic
Bitwise
Commute
Defs
Divisibility
InjSurj
NeZero
Power
Semiconj
Hom
Equiv
Units
Basic
GroupWithZero
Basic
TypeTags
Group
Basic
Defs
Ring
Basic
Defs
Aut
Commute
Embedding
Freiman
GroupAction
GroupInstances
Iterate
NonUnitalAlg
Units
Homology
ShortExact
Abelian
Preadditive
Exact
ImageToKernel
Invertible
Basic
Defs
GroupWithZero
Module
Submodule
Basic
Bilinear
Lattice
Pointwise
Algebra
Basic
BigOperators
DedekindDomain
Equiv
Hom
LinearMap
Opposites
PID
Pi
Prod
Projective
Torsion
ULift
MonoidAlgebra
Basic
Degree
Division
Support
Order
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Power
Group
Abs
Bounds
Defs
InjSurj
Instances
MinMax
OrderIso
Prod
TypeTags
Units
WithTop
Hom
Basic
Monoid
Cancel
Basic
Defs
Canonical
Defs
WithZero
Basic
Defs
Basic
Defs
Lemmas
MinMax
NatCast
OrderDual
Prod
TypeTags
Units
WithTop
Nonneg
Field
Floor
Ring
Positive
Ring
Ring
Abs
Canonical
CharZero
Defs
InjSurj
Lemmas
WithTop
Sub
Canonical
Defs
WithTop
AbsoluteValue
Archimedean
Chebyshev
Floor
Invertible
Kleene
LatticeGroup
Module
Pi
Rearrangement
SMul
ToIntervalMod
WithZero
ZeroLEOne
Polynomial
BigOperators
GroupRingAction
Regular
Basic
Pow
SMul
Ring
Divisibility
Basic
AddAut
Aut
Basic
Commute
CompTypeclasses
Defs
Equiv
Fin
Idempotents
InjSurj
Opposite
Pi
Prod
Regular
Semiconj
ULift
Units
Star
Basic
BigOperators
Center
Module
Order
Pi
Pointwise
Prod
SelfAdjoint
StarAlgHom
Subalgebra
Unitary
Abs
AddTorsor
Associated
Bounds
CovariantAndContravariant
DirectLimit
Free
FreeAlgebra
GeomSum
IndicatorFunction
IsPrimePow
ModEq
NeZero
Opposites
PUnitInstances
Parity
Periodic
Quotient
SMulWithZero
Squarefree
Support
AlgebraicGeometry
PrimeSpectrum
Basic
Maximal
Noetherian
Analysis
Asymptotics
AsymptoticEquivalent
Asymptotics
Theta
Calculus
Conformal
NormedSpace
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
Mul
Pow
Slope
FDeriv
Add
Basic
Bilinear
Comp
Equiv
Linear
Mul
Prod
RestrictScalars
LocalExtr
Basic
Rolle
ContDiff
ContDiffDef
FormalMultilinearSeries
MeanValue
TangentCone
Complex
Arg
Basic
Circle
Conformal
Isometry
RealDeriv
Convex
SpecificFunctions
Basic
Basic
Combination
Function
Hull
Jensen
Normed
Segment
Slope
Star
Strict
StrictConvexSpace
Topology
Uniform
InnerProductSpace
Basic
Orthogonal
PiL2
Projection
Symmetric
LocallyConvex
BalancedCoreHull
Basic
Bounded
WithSeminorms
Normed
Field
Basic
UnitBall
Group
AddCircle
AddTorsor
BallSphere
Basic
Completion
Hom
InfiniteSum
Pointwise
Quotient
Seminorm
Order
Basic
MulAction
NormedSpace
Star
Basic
AddTorsor
AffineIsometry
Banach
Basic
BoundedLinearMaps
Completion
ConformalLinearMap
ContinuousLinearMap
FiniteDimension
IsROrC
LinearIsometry
Multilinear
OperatorNorm
PiLp
Pointwise
Ray
RieszLemma
Units
WithLp
SpecialFunctions
Complex
Arg
Log
Log
Basic
Deriv
Pow
Complex
NNReal
Real
Trigonometric
Angle
Basic
Inverse
Exp
ExpDeriv
SpecificLimits
Basic
Normed
MeanInequalities
MeanInequalitiesPow
Seminorm
CategoryTheory
Abelian
DiagramLemmas
Four
Basic
Exact
Images
NonPreadditive
Opposite
Pseudoelements
Adjunction
Basic
FullyFaithful
Limits
Opposites
Reflective
Bicategory
Basic
Strict
Category
Basic
Cat
Init
Preorder
ULift
ConcreteCategory
Basic
Bundled
BundledHom
Elementwise
ReflectsIso
Filtered
Basic
Functor
Basic
Category
Const
Currying
EpiMono
FullyFaithful
Hom
ReflectsIso
LiftingProperties
Adjunction
Basic
Limits
Constructions
BinaryProducts
EpiMono
Equalizers
FiniteProductsOfBinaryProducts
LimitsOfProductsAndEqualizers
Pullbacks
Preserves
Shapes
BinaryProducts
Biproducts
Equalizers
Kernels
Products
Pullbacks
Terminal
Zero
Basic
Finite
Shapes
NormalMono
Basic
Equalizers
BinaryProducts
Biproducts
Equalizers
FiniteLimits
FiniteProducts
Images
Kernels
Products
Pullbacks
RegularMono
SplitCoequalizer
StrongEpi
Terminal
WidePullbacks
ZeroMorphisms
ZeroObjects
Comma
Cones
Creates
ExactFunctor
Filtered
HasLimits
IsLimit
Opposites
Over
Types
Unit
Linear
Basic
Pi
Basic
Preadditive
AdditiveFunctor
Basic
Biproducts
FunctorCategory
LeftExact
Opposite
Products
Basic
Bifunctor
Subobject
Basic
FactorThru
Lattice
Limits
MonoOver
WellPowered
Arrow
Balanced
CommSq
Comma
Conj
DiscreteCategory
Elementwise
Endomorphism
EpiMono
EqToHom
Equivalence
EssentialImage
EssentiallySmall
FinCategory
FullSubcategory
Groupoid
Iso
IsomorphismClasses
NatIso
NatTrans
Opposites
Over
PEmpty
PUnit
Skeletal
StructuredArrow
Thin
Types
Whiskering
Yoneda
Combinatorics
Additive
SalemSpencer
Quiver
Basic
Path
Push
Symmetric
Composition
Partition
Pigeonhole
Control
Monad
Basic
Traversable
Basic
Instances
Applicative
Basic
Bifunctor
EquivFunctor
Functor
Data
Array
Defs
Bool
Basic
Set
Complex
Basic
Cardinality
Exponential
ExponentialBounds
Module
Order
Countable
Basic
Defs
DFinsupp
Basic
Encodable
ENat
Basic
Lattice
Fin
Tuple
Basic
NatAntidiagonal
Basic
Interval
VecNotation
Finite
Basic
Card
Defs
Set
Finset
Basic
Card
Fin
Finsupp
Fold
Image
Lattice
LocallyFinite
MulAntidiagonal
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
Pointwise
Powerset
Preimage
Prod
Sigma
Sort
Sum
Sym
Finsupp
Antidiagonal
Basic
Defs
Encodable
Fin
Indicator
Interval
Multiset
Notation
Order
Pwo
ToDFinsupp
Fintype
Basic
BigOperators
Card
Fin
Lattice
List
Option
Order
Perm
Pi
Powerset
Prod
Sigma
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Dvd
Basic
Order
Basic
Lemmas
Units
Basic
Bitwise
CharZero
Div
GCD
Interval
LeastGreatest
Lemmas
ModEq
Parity
SuccPred
Units
IsROrC
Basic
Lemmas
List
BigOperators
Basic
Lemmas
Basic
Chain
Count
Cycle
Dedup
Defs
Duplicate
FinRange
Forall2
Indexes
Infix
Join
Lattice
Lex
MinMax
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
Range
Rotate
Sort
Sublists
TFAE
Zip
MLList
Basic
Dedup
Matrix
Basic
Basis
Block
DMatrix
Invertible
Notation
PEquiv
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
NatAntidiagonal
Nodup
Pi
Powerset
Range
Sort
Sum
MvPolynomial
Basic
CommRing
Equiv
Rename
Variables
Nat
Cast
Basic
Commute
Defs
Field
NeZero
Order
Prod
WithTop
Choose
Basic
Cast
Multinomial
Sum
Factorial
Basic
BigOperators
Cast
DoubleFactorial
Factorization
Basic
PrimePow
GCD
Basic
BigOperators
Order
Basic
Lemmas
Basic
Bits
Bitwise
Count
Digits
Factors
ForSqrt
Interval
Lattice
Log
MaxPowDiv
ModEq
Multiplicity
Pairing
Parity
PartENat
Periodic
Pow
Prime
PrimeFin
PrimeNormNum
Set
Size
Sqrt
Squarefree
SuccPred
Totient
Units
WithBot
Nondet
Basic
Num
Basic
Option
Basic
Defs
NAry
PNat
Basic
Defs
Prime
Pi
Algebra
Lex
Polynomial
Degree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
CancelLeads
Coeff
Derivative
Div
EraseLead
Eval
Expand
FieldDivision
Induction
Inductions
Laurent
Lifts
Monic
Monomial
Reverse
RingDivision
Splits
Prod
Basic
Lex
PProd
Rat
Cast
CharZero
Defs
Order
Basic
BigOperators
Defs
Denumerable
Floor
Init
Lemmas
Order
Real
Basic
Cardinality
CauSeq
CauSeqCompletion
ConjugateExponents
ENNReal
NNReal
Pointwise
Sqrt
Set
Intervals
Basic
Disjoint
Group
Image
Infinite
Instances
Monoid
OrdConnected
OrdConnectedComponent
OrderIso
Pi
ProjIcc
UnorderedInterval
WithBotTop
Pairwise
Basic
Lattice
Pointwise
Basic
BigOperators
Finite
Interval
ListOfFn
SMul
Accumulate
Basic
BoolIndicator
Countable
Finite
Function
Functor
Image
Lattice
List
MulAntidiagonal
NAry
Prod
Semiring
Sigma
UnionLift
SetLike
Basic
Setoid
Basic
Sigma
Basic
Lex
String
Defs
Sum
Basic
Order
Sym
Sym2 (file)
Init
Basic
Vector (file)
Basic
ZMod
Algebra
Basic
Defs
Quotient
Bracket
HashMap
KVMap
Opposite
PEquiv
Part
Quot
SProd
Sign
Subtype
Tree
TypeMax
ULift
Dynamics
FixedPoints
Basic
PeriodicPts
FieldTheory
Finite
Basic
GaloisField
Trace
IsAlgClosed
AlgebraicClosure
Basic
Minpoly
Basic
Field
IsIntegrallyClosed
SplittingField
Construction
IsSplittingField
Adjoin
Finiteness
Fixed
Galois
IntermediateField
Normal
NormalClosure
Perfect
PrimitiveElement
RatFunc
Separable
Subfield
Tower
GroupTheory
FreeGroup
Basic
GroupAction
SubMulAction (file)
Pointwise
Basic
BigOperators
ConjAct
Defs
FixingSubgroup
Group
Opposite
Pi
Prod
Quotient
Units
Perm
Cycle
Basic
Type
Basic
Fin
List
Option
Sign
Support
ViaEmbedding
SpecificGroups
Cyclic
Subgroup
Actions
Basic
Finite
MulOpposite
Pointwise
Simple
ZPowers
Submonoid
Basic
Center
Centralizer
Membership
MulOpposite
Operations
Pointwise
ZeroDivisors
Subsemigroup
Basic
Center
Centralizer
Operations
Abelianization
Archimedean
Commutator
Congruence
Coset
Divisible
Exponent
FiniteAbelian
Finiteness
FreeAbelianGroup
Index
MonoidLocalization
NoncommPiCoprod
OrderOfElement
PGroup
QuotientGroup
Solvable
Torsion
Init
Algebra
Classes
Control
Combinators
Lawful
Data
Bool
Basic
Lemmas
Fin
Basic
Int
Basic
Bitwise
CompLemmas
Order
List
Basic
Instances
Lemmas
Nat
Basic
Bitwise
Lemmas
Notation
Ordering
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
Expr (file)
Basic
ReplaceRec
Traverse
Meta (file)
Basic
CongrTheorems
DiscrTree
Simp
EnvExtension
Exception
Linter
Message
LinearAlgebra
AffineSpace
AffineEquiv
AffineMap
AffineSubspace
Basic
Basis
Combination
Independent
Midpoint
MidpointZero
Restrict
Slope
Alternating
Basic
Basis (file)
Bilinear
VectorSpace
Charpoly
Basic
DirectSum
Finsupp
TensorProduct
FreeModule
Finite
Basic
Matrix
Rank
Basic
PID
Rank
StrongRankCondition
Matrix
Charpoly
Basic
Coeff
LinearMap
Minpoly
Adjugate
Basis
BilinearForm
Determinant
GeneralLinearGroup
MvPolynomial
Nondegenerate
NonsingularInverse
Polynomial
Reindex
SesquilinearForm
SpecialLinearGroup
ToLin
ToLinearEquiv
Trace
Multilinear
Basic
Basis
TensorProduct (file)
Tower
Basic
BilinearForm
BilinearMap
Contraction
DFinsupp
Determinant
Dimension
Dual
FiniteDimensional
Finrank
Finsupp
FinsuppVectorSpace
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
LinearIndependent
LinearPMap
Pi
Prod
Projection
Quotient
Ray
SesquilinearForm
Span
StdBasis
TensorProductBasis
Trace
UnitaryGroup
Vandermonde
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Basic
Defs
Fin
Fintype
Functor
List
LocalEquiv
Nat
Option
Set
TransferInstance
Function
Basic
Conjugate
Iterate
Nontrivial
Basic
Defs
Small
Basic
Basic
Denumerable
IsEmpty
Lemmas
Nonempty
Pairwise
Relation
Relator
Unique
UnivLE
Mathport
Attributes
Notation
Rename
NumberTheory
Cyclotomic
Basic
PrimitiveRoots
LegendreSymbol
AddCharacter
NumberField
Basic
Padics
PadicVal
ArithmeticFunction
Divisors
Order
Atoms (file)
Finite
Bounds
Basic
OrderIso
ConditionallyCompleteLattice
Basic
Finset
Group
Filter
Archimedean
AtTopBot
Bases
Basic
Cofinite
CountableInter
EventuallyConst
Extr
Interval
Lift
NAry
Pi
Pointwise
Prod
SmallSets
Subsingleton
Ultrafilter
Heyting
Basic
Hom
Basic
Bounded
CompleteLattice
Lattice
Order
Set
Monotone
Basic
Monovary
Partition
Finpartition
RelIso
Basic
Set
SuccPred
Basic
Limit
Relation
UpperLower
Basic
Antichain
Antisymmetrization
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
CompactlyGenerated
Compare
CompleteBooleanAlgebra
CompleteLattice
CompleteLatticeIntervals
Copy
Cover
Directed
Disjoint
FixedPoints
GaloisConnection
InitialSeg
Iterate
JordanHolder
Lattice
LatticeIntervals
LiminfLimsup
LocallyFinite
Max
MinMax
Minimal
ModularLattice
OmegaCompletePartialOrder
OrderIsoNat
PartialSups
PropInstances
RelClasses
SupClosed
SupIndep
SymmDiff
Synonym
ULift
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
RingTheory
Adjoin
Basic
FG
Field
PowerBasis
Tower
Coprime
Basic
Ideal
Lemmas
DedekindDomain
Basic
Ideal
IntegralClosure
Ideal
Basic
LocalRing
Operations
Over
Prod
Quotient
QuotientOperations
Int
Basic
Localization
Away
Basic
AsSubring
AtPrime
Basic
FractionRing
Ideal
Integer
Integral
LocalizationLocalization
Module
NumDen
Submodule
MvPolynomial
Symmetric
Tower
Polynomial
Cyclotomic
Basic
Eval
Expand
Roots
Eisenstein
Basic
Basic
Content
GaussLemma
IntegralNormalization
Nilpotent
Pochhammer
Quotient
RationalRoot
ScaleRoots
Tower
Vieta
PowerSeries
Basic
RootsOfUnity
Basic
Complex
Minpoly
Subring
Basic
Pointwise
Subsemiring
Basic
Pointwise
Valuation
Basic
AdjoinRoot
AlgebraTower
Algebraic
ChainOfDivisors
Congruence
EisensteinCriterion
EuclideanDomain
FinitePresentation
FiniteType
Finiteness
FractionalIdeal
FreeCommRing
FreeRing
HahnSeries
IntegralClosure
IntegralDomain
IntegrallyClosed
JacobsonIdeal
LaurentSeries
MatrixAlgebra
Multiplicity
Nilpotent
Noetherian
NonZeroDivisors
Norm
PolynomialAlgebra
PowerBasis
Prime
PrincipalIdealDomain
QuotientNilpotent
QuotientNoetherian
SimpleModule
TensorProduct
Trace
UniqueFactorizationDomain
SetTheory
Cardinal
Basic
Cofinality
Continuum
Finite
Ordinal
SchroederBernstein
Ordinal
Arithmetic
Basic
Exponential
FixedPoint
Principal
Tactic
Attr
Core
Register
CancelDenoms
Core
CategoryTheory
Elementwise
Reassoc
Slice
Continuity (file)
Init
GCongr (file)
Core
ForwardAttr
Linarith (file)
Datatypes
Elimination
Frontend
Lemmas
Parsing
Preprocessing
Verification
Monotonicity (file)
Attr
Basic
Lemmas
Nontriviality (file)
Core
NormCast (file)
Tactic
NormNum (file)
Basic
Core
Eq
GCD
Ineq
Inv
OfScientific
Pow
Prime
Result
Positivity (file)
Basic
Core
Relation
Rfl
Symm
Trans
Ring (file)
Basic
RingNF
Simps
Basic
NotationClass
Abel
ApplyCongr
ApplyFun
ApplyWith
Backtrack
Basic
ByContra
Cache
Cases
CasesM
Choose
Classical
Clear!
ClearExcept
Clear_
Coe
Common
ComputeDegree
Congr!
Congrm
Constructor
Contrapose
Conv
Convert
Core
DefEqTransformations
DeriveToExpr
Eqns
Existsi
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
Have
HaveI
HelpCmd
HigherOrder
InferParam
Inhabit
IntervalCases
IrreducibleDef
LeftRight
LibrarySearch
Lift
LinearCombination
Lint
MkIffOfInductiveProp
NthRewrite
Observe
PPWithUniv
PermuteGoals
PrintPrefix
ProjectionNotation
Propose
PushNeg
RSuffices
Recover
Rename
RenameBVar
Replace
Rewrites
RunCmd
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SolveByElim
SplitIfs
Spread
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TermCongr
ToAdditive
ToExpr
ToLevel
Trace
TryThis
TypeCheck
UnsetOption
Use
Variable
WLOG
Zify
Topology
Algebra
Group
Basic
InfiniteSum
Basic
Module
Order
Real
Ring
Module
Basic
Determinant
FiniteDimension
LocallyConvex
Multilinear
Simple
Star
StrongTopology
Order
Archimedean
Compact
ExtendFrom
Field
Group
IntermediateValue
LeftRight
LiminfLimsup
MonotoneContinuity
MonotoneConvergence
ProjIcc
Rolle
T5
Ring
Basic
Ideal
Affine
Algebra
ConstMulAction
Constructions
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Monoid
MulAction
Polynomial
Star
StarSubalgebra
UniformConvergence
UniformGroup
UniformMulAction
UniformRing
Bornology
Basic
Constructions
Hom
Compactness
Compact
LocallyCompact
SigmaCompact
Connected
Basic
LocallyConnected
PathConnected
TotallyDisconnected
ContinuousFunction
Basic
EMetricSpace
Basic
Instances
AddCircle
ENNReal
Int
Matrix
NNReal
Nat
Rat
Real
RealVectorSpace
Sign
MetricSpace
Algebra
Antilipschitz
Baire
Basic
Completion
Equicontinuity
HausdorffDistance
IsometricSMul
Isometry
Lipschitz
Order (file)
Basic
Sets
Closeds
Compacts
Opens
UniformSpace
AbstractCompletion
Basic
Cauchy
Compact
CompleteSeparated
Completion
Equicontinuity
Equiv
Pi
Separation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
Bases
Basic
Clopen
CompactOpen
Constructions
ContinuousOn
DenseEmbedding
DiscreteSubset
ExtendFrom
GDelta
Homeomorph
Inseparable
Irreducible
LocalExtr
LocalHomeomorph
LocallyFinite
Maps
NhdsSet
NoetherianSpace
QuasiSeparated
Separation
Sequences
Sober
Support
UnitInterval
Util
AddRelatedDecl
AssertExists
AtomM
CompileInductive
CountHeartbeats
DischargerAsTactic
Imports
MemoFix
Qq
Syntax
SynthesizeUsing
Tactic
WhatsNew
WithWeakNamespace
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
Data
Array
Init
Basic
Lemmas
Basic
Lemmas
Match
Merge
BinomialHeap (file)
Basic
Lemmas
BitVec (file)
Basic
Fin
Init
Lemmas
Basic
Lemmas
HashMap (file)
Basic
WF
Int
Basic
DivMod
Lemmas
List
Init
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
Char
DList
Ord
PairingHeap
Lean
Elab
Tactic
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
LCtx
SavedState
UnusedNames
Util
Path
AttributeExtra
Command
CoreM
Delaborator
Expr
Float
Format
HashMap
HashSet
InfoTree
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
Ext
Lemmas
Relation
Rfl
Symm
Alias
Basic
ByCases
Case
CoeExt
Congr
Exact
GuardExpr
GuardMsgs
HaveI
Instances
LabelAttr
NoMatch
OpenPrivate
PrintDependents
RCases
Replace
SeqFocus
ShowTerm
SimpTrace
Simpa
SqueezeScope
TryThis
Unreachable
Where
Test
Internal
DummyLabelAttr
Util
ExtendedBinder
LibraryNote
Pickle
TermUnsafe
Logic
WF

Color scheme