General documentation

index
foundational types

Library

Aesop (file)
Builder
Apply
Basic
Cases
Constructors
Default
Forward
NormSimp
Tactic
Unfold
BuiltinRules (file)
ApplyHyps
Assumption
DestructProducts
Ext
Intros
Rfl
Split
Subst
Forward
Match (file)
Types
State (file)
ApplyGoalDiff
Initial
LevelIndex
PremiseIndex
RuleInfo
SlotIndex
Substitution
Frontend
Extension (file)
Init
Attribute
Basic
Command
RuleExpr
Saturate
Tactic
Index (file)
Basic
DiscrTreeConfig
Forward
RulePattern
Options (file)
Internal
Public
RPINF (file)
Basic
Rule (file)
Basic
Forward
Name
RulePattern (file)
Cache
RuleSet (file)
Filter
Member
Name
RuleTac (file)
Forward (file)
Basic
Apply
Basic
Cases
Descr
ElabRuleTerm
FVarIdSubst
GoalDiff
Preprocess
RuleTerm
Tactic
Script
Check
CtorNames
GoalWithMVars
Main
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)
Data (file)
ForwardRuleMatches
AddRapp
Check
ExtractProof
ExtractScript
Free
RunMetaM
State
Tracing
Traversal
TreeM
UnsafeQueue
Util
Tactic (file)
Ext
Unfold
Basic
EqualUpToIds
UnionFind
UnorderedArraySet
BaseM
Check
Constants
ElabM
Exception
Main
Nanos
Percent
Saturate
Tracing
Batteries
Classes
Order
RatCast
CodeAction (file)
Attr
Basic
Deprecated
Misc
Control
ForInStep
Basic
Lemmas
Nondet
Basic
Data
Array
Init
Lemmas
Basic
Merge
BinomialHeap
Basic
List
Init
Lemmas
Basic
Count
Lemmas
Pairwise
Perm
MLList
Basic
Nat
Basic
Gcd
Rat
Basic
Lemmas
String
Basic
NameSet
Lean
Meta
Basic
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
UnusedNames
AttributeExtra
Except
Expr
HashSet
MonadBacktrack
NameMapAttribute
PersistentHashMap
PersistentHashSet
Position
Syntax
TagAttribute
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
Alias
Basic
Congr
Exact
HelpCmd
Init
OpenPrivate
PermuteGoals
SeqFocus
Trans
Unreachable
Util
Cache
ExtendedBinder
LibraryNote
ProofWanted
Logic
WF
ImportGraph
Imports
RequiredModules
Init (file)
Control (file)
Lawful (file)
Basic
Instances
Lemmas
Basic
EState
Except
ExceptCps
Id
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Lex (file)
Basic
Lemmas
QSort (file)
Basic
Subarray (file)
Split
Attach
Basic
BasicAux
BinSearch
Bootstrap
Count
DecidableEq
Erase
Extract
FinRange
Find
GetLit
InsertIdx
InsertionSort
Lemmas
MapIdx
Mem
Monadic
OfFn
Perm
Range
Set
TakeDrop
Zip
BitVec (file)
Basic
BasicAux
Bitblast
Folds
Lemmas
ByteArray (file)
Basic
Char (file)
Basic
Lemmas
Fin (file)
Basic
Bitwise
Fold
Iterate
Lemmas
Log2
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Int (file)
Bitwise (file)
Basic
Lemmas
DivMod (file)
Basic
Bootstrap
Lemmas
Basic
Compare
Cooper
Gcd
Lemmas
LemmasAux
Linear
OfNat
Order
Pow
List (file)
Nat (file)
BEq
Basic
Count
Erase
Find
InsertIdx
Modify
Pairwise
Perm
Range
Sublist
TakeDrop
Sort (file)
Basic
Impl
Lemmas
Attach
Basic
BasicAux
Control
Count
Erase
FinRange
Find
Impl
Lemmas
Lex
MapIdx
MinMax
Monadic
Notation
OfFn
Pairwise
Perm
Range
Sublist
TakeDrop
ToArray
ToArrayImpl
Zip
Nat (file)
Bitwise (file)
Basic
Lemmas
Div (file)
Basic
Lemmas
Basic
Compare
Control
Dvd
Fold
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Power2
SOM
Simproc
Option (file)
Attach
Basic
BasicAux
Coe
Instances
Lemmas
List
Monadic
Range (file)
Basic
Lemmas
SInt (file)
Basic
Bitwise
Float
Float32
Lemmas
String (file)
Basic
Extra
Lemmas
Sum (file)
Basic
Lemmas
ToString (file)
Basic
Macro
UInt (file)
Basic
BasicAux
Bitwise
Lemmas
Log2
Vector (file)
Attach
Basic
Count
DecidableEq
Erase
Extract
FinRange
Find
InsertIdx
Lemmas
Lex
MapIdx
Monadic
OfFn
Perm
Range
Zip
AC
BEq
Basic
Bool
Cast
Channel
Float
Float32
Function
Hashable
NeZero
OfScientific
Ord
PLift
Prod
Queue
RArray
Random
Repr
Stream
Subtype
ULift
Zero
Grind (file)
CommRing (file)
Basic
BitVec
Int
Poly
SInt
UInt
Cases
Ext
Lemmas
Norm
Offset
PP
Propagator
Tactics
Util
Internal (file)
Order (file)
Basic
Lemmas
Tactic
Omega (file)
Coeffs
Constraint
Int
IntList
LinearCombo
Logic
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
BinderNameHint
BinderPredicates
ByCases
Classical
Coe
Conv
Core
Dynamic
Ext
GetElem
Guard
Hints
MacroTrace
Meta
MetaTypes
Notation
NotationExtra
Prelude
PropLemmas
RCases
ShareCommon
SimpLemmas
Simproc
SizeOf
SizeOfLemmas
Syntax
Tactics
TacticsExtra
Task
Try
Util
WF
WFTactics
While
Iwasawalib (file)
Algebra
CompleteGroupAlgebra
Basic
Exact
Basic
KerCokerComp
FieldTheory
ZpExtension
Basic
NumberTheory
ZpExtension
Basic
ClassGroup
RingTheory
CharacteristicIdeal
Basic
PowerSeries
WeierstrassPreparation
PseudoNull
Basic
CharacteristicIdeal
StructureTheorem
Lake (file)
Build (file)
Job (file)
Basic
Monad
Register
Target (file)
Basic
Fetch
Actions
Common
Context
Data
Executable
Facets
Fetch
Imports
Index
Info
Key
Library
Module
Package
Run
Store
Targets
Topological
Trace
CLI
Actions
Build
Error
Config (file)
ConfigDecl
ConfigTarget
Context
Defaults
Dependency
Dynlib
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InputFile
InputFileConfig
InstallPath
Kinds
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Meta
Module
Monad
Opaque
OutFormat
Package
Pattern
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
AttributesCore
Config
DeclUtil
Extensions
Key
Meta
Package
Require
Script
Syntax
Targets
VerLit
Load
Config
Manifest
Toml (file)
Data
DateTime
Dict
Value
Elab (file)
Expression
Value
Grammar
Load
ParserUtil
Util
Binder
Casing
Compare
Cycle
DRBMap
Date
EStateT
EquipT
Error
Exit
Family
FilePath
Git
IO
JsonObject
Lift
List
Lock
Log
Message
Name
NativeLib
Opaque
OpaqueType
OrdHashSet
OrderedTagAttribute
Proc
RBArray
Store
StoreInsts
Sugar
Task
Version
Reservoir
Version
Lean (file)
Compiler (file)
IR (file)
Basic
Borrow
Boxing
Checker
CompilerM
CtorLayout
ElimDeadBranches
ElimDeadVars
EmitC
EmitLLVM
EmitUtil
ExpandResetReuse
Format
FreeVars
LLVMBindings
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
InferType
Internalize
JoinPoints
LCtx
LambdaLifting
Level
Main
MonadScope
MonoTypes
OtherDecl
PassManager
Passes
PhaseExt
PrettyPrinter
Probing
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
CancelParams
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Window
Workspace
Xml (file)
Basic
Parser
Array
AssocList
DeclarationRange
Format
FuzzyMatching
HashMap
HashSet
JsonRpc
KVMap
LBool
LOption
Name
NameMap
NameTrie
OpenDecl
Options
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RArray
RBMap
RBTree
SMap
SSet
Trie
DocString (file)
Add
Extension
Links
Elab (file)
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
ToExpr
TypeName
Util
InfoTree (file)
InlayHints
Main
Types
PreDefinition (file)
Nonrec
Eqns
PartialFixpoint (file)
Eqns
Induction
Main
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndGroupInfo
IndPred
Main
Preprocess
RecArgInfo
SmartUnfolding
WF (file)
Basic
Eqns
Fix
FloatRecApp
GuessLex
Main
PackMutual
Preprocess
Rel
Unfold
Basic
EqUnfold
Eqns
FixedParams
Main
MkInhabitant
Mutual
TerminationHint
TerminationMeasure
Quotation (file)
Precheck
Util
Tactic (file)
BVDecide (file)
Frontend (file)
BVDecide (file)
Reflect
ReifiedBVExpr
ReifiedBVLogical
ReifiedBVPred
ReifiedLemmas
Reify
SatAtBVLogical
Normalize (file)
AC
AndFlatten
ApplyControlFlow
Basic
EmbeddedConstraint
Enums
IntToBitVec
Rewrite
ShortCircuit
Simproc
Structures
TypeAnalysis
Attr
BVCheck
BVTrace
LRAT
LRAT (file)
Trim
External
Conv (file)
Basic
Change
Congr
Delta
Lets
Pattern
Rewrite
Simp
Unfold
Omega (file)
Core
Frontend
MinNatAbs
OmegaM
AsAuxLemma
Basic
BoolToPropSimps
BuiltinTactic
Calc
Change
Classical
Config
Congr
Delta
DiscrTreeKey
Doc
ElabTerm
ExposeNames
Ext
FalseOrByContra
Generalize
Grind
Guard
Induction
Injection
Lets
LibrarySearch
Location
Match
Meta
Monotonicity
NormCast
RCases
Repeat
Rewrite
Rewrites
Rfl
ShowTerm
Simp
SimpArith
SimpTrace
Simpa
Simproc
SolveByElim
Split
Symm
TreeTacAttr
Try
Unfold
App
Arg
Attributes
AutoBound
AuxDef
BinderPredicates
Binders
BindersUtil
BuiltinCommand
BuiltinEvalCommand
BuiltinNotation
BuiltinTerm
Calc
CheckTactic
Command
ComputedFields
Config
DeclModifiers
DeclNameGen
DeclUtil
Declaration
DeclarationRange
DefView
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
GuardMsgs
Import
Inductive
InfoTrees
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
MatchExpr
Mixfix
MutualDef
MutualInductive
Notation
Open
ParseImportsFast
PatternVar
Print
RecAppSyntax
RecommendedSpelling
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Term
Time
Util
Language
Lean (file)
Types
Basic
Util
Linter (file)
Basic
Builtin
ConstructorAsVariable
Deprecated
List
MissingDocs
Omit
UnusedVariables
Util
Meta (file)
ArgsPacker (file)
Basic
Constructions (file)
BRecOn
CasesOn
NoConfusion
RecOn
Match (file)
MatcherApp (file)
Basic
Transform
Basic
CaseArraySizes
CaseValues
MVarRenaming
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
Tactic (file)
AC (file)
Main
Grind (file)
Arith (file)
CommRing (file)
DenoteExpr
EqCnstr
Internalize
Inv
Poly
Proof
Reify
RingId
ToExpr
Types
Util
Var
Cutsat (file)
DvdCnstr
EqCnstr
Foreign
Inv
LeCnstr
MBTC
Model
Nat
Norm
Proof
Search
SearchM
Types
Util
Var
Offset (file)
Main
Model
Proof
Types
Util
Internalize
Inv
Main
Model
ProofUtil
Types
Util
Attr
Beta
Canon
Cases
CasesMatch
Combinators
Core
Ctor
Diseq
EMatch
EMatchTheorem
ENodeKey
EqResolution
Ext
ExtAttr
ForallProp
Injection
Internalize
Intro
Inv
Lookahead
MBTC
Main
MarkNestedProofs
MatchCond
MatchDiscrOnly
PP
Parser
Proj
Proof
Propagate
PropagatorAttr
ProveEq
RevertAll
Simp
SimpUtil
Solve
Split
Types
Util
Simp (file)
Arith (file)
Int (file)
Basic
Simp
Nat (file)
Basic
Simp
Util
BuiltinSimprocs (file)
Array
BitVec
Char
Core
Fin
Int
List
Nat
SInt
String
UInt
Util
Attr
Diagnostics
Main
RegisterCommand
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Simproc
Types
Try (file)
Collect
Acyclic
Apply
Assert
Assumption
AuxLemma
Backtrack
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
ExposeNames
Ext
FVarSubst
FunInd
FunIndCollect
FunIndInfo
Generalize
IndependentOf
Induction
Injection
Intro
Lets
LibrarySearch
NormCast
Refl
Rename
Repeat
Replace
Revert
Rewrite
Rewrites
Rfl
SolveByElim
Split
SplitIf
Subst
Symm
TryThis
Unfold
UnifyEq
Util
ACLt
AbstractMVars
AbstractNestedProofs
AppBuilder
Basic
BinderNameHint
Canonicalizer
Check
CheckTactic
Closure
Coe
CoeAttr
CollectFVars
CollectMVars
CompletionName
CongrTheorems
CtorRecognizer
DecLevel
Diagnostics
DiscrTree
DiscrTreeTypes
Eqns
Eval
ExprDefEq
ExprLens
ExprTraverse
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetUnfoldableConst
GlobalInstances
IndPredBelow
Inductive
InferType
Injective
Instances
IntInstTesters
Iterator
KAbstract
KExprMap
LazyDiscrTree
LevelDefEq
LitValues
MatchUtil
NatInstTesters
Offset
Order
PPGoal
PProdN
RecursorInfo
Reduce
ReduceEval
SizeOf
Sorry
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (file)
Tactic (file)
Doc
Term (file)
Doc
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
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
UnknownIdentifier
Completion (file)
CompletionCollectors
CompletionInfoSelection
CompletionItemData
CompletionResolution
CompletionUtils
EligibleHeaderDecls
ImportCompletion
SyntheticCompletion
FileWorker (file)
ExampleHover
InlayHints
RequestHandling
SemanticHighlighting
SetupFile
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
Test (file)
Cancel
Runner
AsyncList
FileSource
GoTo
InfoUtils
References
RequestCancellation
Requests
ServerTask
Snapshots
Utils
Watchdog
Util (file)
CollectAxioms
CollectFVars
CollectLevelMVars
CollectLevelParams
CollectMVars
Diff
FVarSubset
FileSetupInfo
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
Heartbeats
InstantiateLevelParams
LakePath
LeanOptions
MonadBacktrack
MonadCache
NumApps
NumObjs
OccursCheck
PPExt
Path
Paths
Profile
Profiler
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SCC
SafeExponentiation
SearchPath
ShareCommon
Sorry
SortExprs
TestExtern
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
EnvExtension
Environment
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LabelAttribute
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
Namespace
PremiseSelection
PrivateName
ProjFns
ReducibilityAttrs
Replay
ReservedNameAction
ResolveName
Runtime
ScopedEnvExtension
Structure
SubExpr
Syntax
ToExpr
ToLevel
LeanSearchClient (file)
Basic
LoogleSyntax
Syntax
Mathlib
Algebra
AddTorsor
Basic
Defs
Algebra
Hom (file)
Rat
Spectrum (file)
Basic
Subalgebra
Basic
Directed
Lattice
Operations
Pointwise
Prod
Tower
Basic
Bilinear
Defs
Equiv
Field
NonUnitalHom
NonUnitalSubalgebra
Operations
Opposite
Pi
Prod
Rat
RestrictScalars
Tower
BigOperators
Finsupp
Basic
Fin
Group
Finset
Basic
Defs
Indicator
Lemmas
Pi
Piecewise
Powerset
Preimage
Sigma
List
Basic
Defs
Lemmas
Multiset
Basic
Defs
GroupWithZero
Action
Finset
Ring
Finset
List
Multiset
Associated
Balance
Expect
Field
Fin
Finprod
Intervals
Module
NatAntidiagonal
Option
Pi
RingEquiv
WithTop
Category
Grp
Abelian
Basic
Colimits
EpiMono
EquivalenceGroupAddGroup
ForgetCorepresentable
Kernels
Limits
Preadditive
ZModuleEquivalence
ModuleCat
Abelian
Basic
Biproducts
Colimits
EpiMono
Kernels
Limits
MonCat
Basic
ForgetCorepresentable
Limits
Ring
Basic
Colimits
Constructions
Instances
Limits
CharP
Algebra
Basic
Defs
Frobenius
Invertible
Lemmas
Quotient
Reduced
Two
CharZero
Defs
Infinite
Quotient
Colimit
DirectLimit
Module
DirectSum
Basic
Decomposition
Finsupp
Module
Divisibility
Basic
Hom
Units
Equiv
TransferInstance
EuclideanDomain
Basic
Defs
Field
Int
Field
Subfield
Basic
Defs
Basic
Defs
Equiv
IsField
NegOnePow
Opposite
Periodic
Rat
ZMod
FreeMonoid
Basic
UniqueProds
GCDMonoid
Basic
Finset
Multiset
Nat
Group
Action
Pointwise
Set
Basic
Basic
Defs
End
Faithful
Hom
Opposite
Pi
Pretransitive
Prod
TypeTags
Units
Commute
Basic
Defs
Hom
Units
Equiv
Basic
Defs
Opposite
TypeTags
Fin
Basic
Tuple
Hom
Basic
CompTypeclasses
Defs
End
Instances
Int
Defs
Even
Units
Invertible
Basic
Defs
Irreducible
Defs
Lemmas
Nat
Defs
Even
Hom
Range
Units
Pi
Basic
Lemmas
Pointwise
Finset
Basic
Scalar
Set
Basic
BigOperators
Card
Finite
Lattice
ListOfFn
Scalar
Semiconj
Basic
Defs
Units
Subgroup
ZPowers
Basic
Lemmas
Actions
Basic
Defs
Finite
Ker
Lattice
Map
MulOpposite
MulOppositeLemmas
Order
Pointwise
Submonoid
Basic
BigOperators
Defs
DistribMulAction
Membership
MulAction
MulOpposite
Operations
Pointwise
Subsemigroup
Basic
Defs
Membership
Operations
TypeTags
Basic
Finite
Hom
UniqueProds
Basic
Units
Basic
Defs
Equiv
Hom
Opposite
WithOne
Defs
AddChar
Basic
Center
Commutator
Conj
Defs
Embedding
End
Even
Ext
FiniteSupport
Graph
Idempotent
Indicator
InjSurj
NatPowAssoc
Opposite
PUnit
Prod
Support
Torsion
ULift
GroupWithZero
Action
Pointwise
Set
Basic
Defs
End
Opposite
Pi
Prod
Units
Pointwise
Set
Basic
Submonoid (file)
Pointwise
Primal
Units
Basic
Equiv
Lemmas
Associated
Basic
Center
Commute
Defs
Divisibility
Equiv
Hom
Idempotent
Indicator
InjSurj
Invertible
Nat
NeZero
NonZeroDivisors
Opposite
Pi
Prod
Semiconj
Subgroup
ULift
WithZero
Homology
ShortComplex
Ab
Abelian
Basic
ConcreteCategory
Exact
ExactFunctor
Homology
LeftHomology
Limits
ModuleCat
PreservesHomology
QuasiIso
RightHomology
ShortExact
SnakeLemma
ExactSequence
ImageToKernel
Module
Equiv
Basic
Defs
Opposite
LinearMap
Basic
Defs
End
Prod
Star
LocalizedModule
Basic
Exact
Int
IsLocalization
Submodule
Submodule
Basic
Bilinear
Defs
EqLocus
Equiv
Invariant
IterateMapComap
Ker
Lattice
LinearMap
Map
Pointwise
Range
RestrictScalars
ZLattice
Basic
Covolume
Basic
BigOperators
DedekindDomain
Defs
End
Hom
MinimalAxioms
NatInt
Opposite
PID
PUnit
Pi
Prod
Projective
Rat
RingHom
SpanRank
Torsion
ULift
ZMod
MonoidAlgebra
Basic
Defs
Degree
Division
MapDomain
NoZeroDivisors
Support
MvPolynomial
Basic
CommRing
Degrees
Equiv
Eval
Monad
Rename
Supported
Variables
NoZeroSMulDivisors
Basic
Defs
Pi
Notation (file)
Defs
Lemmas
Pi
Prod
Order
AbsoluteValue
Basic
Euclidean
Antidiag
Finsupp
Pi
Prod
Archimedean
Basic
BigOperators
Group
Finset
List
LocallyFinite
Multiset
Ring
Finset
List
Multiset
Expect
CauSeq
Basic
BigOperators
Completion
Field
Basic
Canonical
Defs
InjSurj
Pointwise
Power
Rat
Floor
Defs
Ring
Semiring
Group
Pointwise
Bounds
Interval
Unbundled
Abs
Basic
Int
Abs
Action
Basic
Defs
DenselyOrdered
Finset
Indicator
InjSurj
Instances
Int
Lattice
MinMax
Multiset
Nat
Opposite
OrderIso
PiLex
PosPart
Synonym
TypeTags
Units
GroupWithZero
Action
Synonym
Unbundled
Basic
Defs
OrderIso
Canonical
Finset
Submonoid
Synonym
Hom
Basic
Monoid
Ring
Interval
Finset
Basic
SuccPred
Set
Group
Instances
Monoid
Module
Algebra
Defs
OrderedSMul
Pointwise
Rat
Synonym
Monoid
Canonical
Defs
Unbundled
Basic
Defs
ExistsOfLE
MinMax
OrderDual
Pow
TypeTags
WithTop
Basic
Defs
NatCast
OrderDual
TypeTags
Units
WithTop
Nonneg
Basic
Field
Floor
Lattice
Ring
Positive
Ring
Ring
Unbundled
Basic
Rat
Abs
Basic
Canonical
Cast
Defs
Idempotent
InjSurj
Int
Nat
Pow
Rat
Synonym
WithTop
Star
Basic
Sub
Unbundled
Basic
Basic
Defs
WithTop
SuccPred (file)
WithBot
AddGroupWithTop
Invertible
Kleene
Monovary
PartialSups
Pi
Round
ToIntervalMod
ZeroLEOne
Polynomial
Degree
Definitions
Domain
Lemmas
Monomial
Operations
SmallDegree
Support
TrailingDegree
Units
Eval
Algebra
Coeff
Defs
Degree
SMul
Subring
Module
AEval
Basic
AlgebraMap
Basic
BigOperators
CancelLeads
Coeff
Derivative
Div
EraseLead
Expand
FieldDivision
GroupRingAction
Identities
Inductions
Laurent
Lifts
Monic
Monomial
Reverse
RingDivision
Roots
Splits
Prime
Defs
Lemmas
Regular
Basic
Pow
SMul
Ring
Action
Pointwise
Set
Basic
ConjAct
End
Field
Group
Invariant
Rat
Subobjects
Divisibility
Basic
Hom
Basic
Defs
Int
Defs
Parity
Units
Pointwise
Set
Submonoid (file)
Basic
Pointwise
Subring
Basic
Defs
Pointwise
Units
Subsemiring
Basic
Defs
Pointwise
AddAut
Associated
Aut
Basic
Center
Centralizer
CharZero
Commute
CompTypeclasses
Defs
Equiv
Fin
GrindInstances
Idempotent
InjSurj
Invertible
Nat
NegOnePow
NonZeroDivisors
Opposite
PUnit
Parity
Periodic
Pi
Prod
Rat
Regular
Semiconj
ULift
Units
Small
Group
Squarefree
Basic
Star
Basic
BigOperators
Center
Module
NonUnitalSubalgebra
Pi
Pointwise
Prod
Rat
SelfAdjoint
StarAlgHom
StarRingHom
Subalgebra
Unitary
Exact
FreeAlgebra
GeomSum
IsPrimePow
ModEq
NeZero
Opposites
QuadraticDiscriminant
Quotient
Analysis
Analytic
Basic
CPolynomial
CPolynomialDef
ChangeOrigin
Composition
Constructions
Inverse
IsolatedZeros
Linear
OfScalars
Uniqueness
Within
Asymptotics
AsymptoticEquivalent
Defs
Lemmas
TVS
Theta
BoxIntegral
Box
Basic
SubboxInduction
Partition
Additive
Basic
Filter
Measure
Split
SubboxInduction
Tagged
Basic
DivergenceTheorem
Integrability
UnitPartition
CStarAlgebra
Basic
Calculus
ContDiff
Basic
Defs
FTaylorSeries
FaaDiBruno
Operations
RCLike
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
MeanValue
Mul
Polynomial
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
LocalExtr
Basic
Rolle
DSlope
DiffContOnCl
FormalMultilinearSeries
LogDeriv
MeanValue
ParametricIntegral
TangentCone
Complex
Polynomial
Basic
Asymptotics
Basic
CauchyIntegral
Convex
Liouville
ReImTopology
RealDeriv
Convex
Cone
Basic
Extension
SpecificFunctions
Basic
Deriv
Basic
Body
Combination
Deriv
EGauge
Function
Gauge
Hull
Jensen
Measure
Mul
Segment
Slope
Star
Strict
Topology
TotallyBounded
InnerProductSpace
Basic
Continuous
Defs
GramSchmidtOrtho
LinearMap
Orientation
Orthogonal
Orthonormal
PiL2
ProdL2
Projection
Subspace
Symmetric
LocallyConvex
AbsConvex
BalancedCoreHull
Basic
Bounded
Polar
WithSeminorms
Normed
Affine
AddTorsor
AddTorsorBases
Isometry
Algebra
Exponential
Field
Basic
Lemmas
ProperSpace
Group
AddCircle
AddTorsor
Basic
Bounded
Completion
Constructions
Continuity
Hom
InfiniteSum
Int
Lemmas
Pointwise
Quotient
Rat
Seminorm
Subgroup
Submodule
Uniform
Lp
PiLp
ProdLp
WithLp
Module
Basic
Completion
Convex
Dual
FiniteDimension
Span
Operator
Banach
BoundedLinearMaps
ContinuousLinearMap
LinearIsometry
Order
Basic
Lattice
Ring
Basic
InfiniteSum
Lemmas
Units
MulAction
NormedSpace
HahnBanach
Extension
SeparatingDual
Separation
Multilinear
Basic
Curry
OperatorNorm
Asymptotics
Basic
Bilinear
Completeness
Mul
NNNorm
NormedSpace
Extend
FunctionSeries
IndicatorFunction
Pointwise
RCLike
Real
RieszLemma
SphereNormEquiv
RCLike
Basic
Lemmas
SpecialFunctions
Complex
Arg
CircleMap
Log
LogDeriv
Gamma
Basic
BohrMollerup
Deriv
Gaussian
GaussianIntegral
Log
Base
Basic
Deriv
NegMulLog
Pow
Asymptotics
Complex
Continuity
Deriv
NNReal
Real
Trigonometric
Angle
Arctan
ArctanDeriv
Basic
Bounds
Complex
ComplexDeriv
Deriv
Inverse
Exp
ExpDeriv
Exponential
ImproperIntegrals
Integrals
JapaneseBracket
NonIntegrable
PolarCoord
Sqrt
SpecificLimits
Basic
Normed
RCLike
MeanInequalities
MeanInequalitiesPow
MellinTransform
Oscillation
Seminorm
CategoryTheory
Abelian
Basic
Exact
Images
NonPreadditive
Opposite
Refinements
Adjunction
Basic
Comma
FullyFaithful
Limits
Mates
Reflective
Restrict
Bicategory
Basic
Strict
Category
Basic
Cat
Init
Preorder
ULift
Comma
Over
Basic
Pullback
StructuredArrow
Basic
Arrow
Basic
ConcreteCategory
Basic
Bundled
Elementwise
EpiMono
ReflectsIso
Discrete
Basic
Filtered
Basic
FinCategory
AsType
Basic
Functor
ReflectsIso
Basic
Basic
Category
Const
Currying
EpiMono
FullyFaithful
Hom
TwoSquare
LiftingProperties
Adjunction
Basic
Limits
ConcreteCategory
Basic
Constructions
BinaryProducts
EpiMono
Equalizers
FiniteProductsOfBinaryProducts
LimitsOfProductsAndEqualizers
Pullbacks
ZeroObjects
FunctorCategory
Basic
Preserves
Creates
Finite
Shapes
BinaryProducts
Biproducts
Equalizers
Kernels
Products
Pullbacks
Terminal
Zero
Basic
Finite
Limits
Shapes
NormalMono
Basic
Equalizers
Pullback
CommSq
Cospan
HasPullback
Iso
Mono
Pasting
PullbackCone
BinaryBiproducts
BinaryProducts
Biproducts
ConcreteCategory
Equalizers
Equivalence
FiniteLimits
FiniteProducts
Images
IsTerminal
Kernels
Multiequalizer
Products
RegularMono
SplitCoequalizer
SplitEqualizer
StrictInitial
StrongEpi
Terminal
WidePullbacks
ZeroMorphisms
ZeroObjects
Types
Colimits
Filtered
Images
Limits
Shapes
Yoneda
ConeCategory
Cones
Creates
ExactFunctor
Filtered
HasLimits
IsLimit
Opposites
Yoneda
Linear
Basic
Monad
Algebra
Basic
Products
MorphismProperty
Basic
Composition
Concrete
Factorization
ObjectProperty
Basic
ClosedUnderIsomorphisms
FullSubcategory
Pi
Basic
Preadditive
Injective
Basic
Projective
Basic
AdditiveFunctor
Basic
Biproducts
FunctorCategory
LeftExact
Opposite
Products
Basic
Unitor
Subobject
Basic
FactorThru
Lattice
Limits
MonoOver
WellPowered
Balanced
CommSq
ComposableArrows
Conj
Elementwise
Endomorphism
EpiMono
EqToHom
Equivalence
EssentialImage
EssentiallySmall
FullSubcategory
Groupoid
HomCongr
InducedCategory
Iso
IsomorphismClasses
NatIso
NatTrans
Opposites
PEmpty
PUnit
Retract
Skeletal
Thin
Types
Whiskering
Yoneda
Combinatorics
Enumerative
Composition
Partition
Quiver
Basic
Path
Prefunctor
Push
Symmetric
Pigeonhole
Control
Monad
Basic
Traversable
Basic
Applicative
Basic
Bifunctor
Combinators
EquivFunctor
Functor
ULift
Data
Array
Defs
Bool
Basic
Set
Complex
Basic
BigOperators
Cardinality
Exponential
FiniteDimensional
Module
Norm
Order
Trigonometric
Countable
Basic
Defs
Small
DFinsupp
BigOperators
Defs
Encodable
Ext
Lex
Module
NeLocus
Order
Sigma
Small
Submonoid
WellFounded
ENNReal
Action
Basic
BigOperators
Holder
Inv
Lemmas
Operations
Real
ENat
Basic
Defs
Lattice
EReal
Basic
Inv
Operations
Fin
Tuple
Basic
NatAntidiagonal
Reflection
Basic
Rev
VecNotation
Finite
Card
Defs
Prod
Set
Sigma
Sum
Finset
Lattice
Basic
Fold
Lemmas
Prod
Union
Attach
Attr
Basic
BooleanAlgebra
Card
Dedup
Defs
Density
Disjoint
Empty
Erase
Filter
Fin
Fold
Image
Insert
Max
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
Piecewise
Powerset
Preimage
Prod
Range
SDiff
Sigma
Sort
Sum
Sym
SymmDiff
Union
Update
Finsupp
Antidiagonal
Basic
Defs
Encodable
Ext
Fin
Fintype
Indicator
Lex
Multiset
Order
SMul
SMulWithZero
Single
ToDFinsupp
Weight
WellFounded
Fintype
Basic
BigOperators
Card
CardEmbedding
Defs
EquivFin
Fin
Inv
Lattice
List
OfMap
Option
Order
Perm
Pi
Pigeonhole
Powerset
Prod
Quotient
Sets
Sigma
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Int
Cast
Basic
Defs
Field
Lemmas
Pi
Prod
Order
Basic
Units
AbsoluteValue
Associated
Basic
CharZero
ConditionallyCompleteOrder
DivMod
GCD
Init
Interval
LeastGreatest
Log
ModEq
Notation
Sqrt
SuccPred
List
Perm
Basic
Lattice
Subperm
Basic
Chain
Count
Cycle
Dedup
Defs
Duplicate
FinRange
Flatten
Forall2
Induction
Infix
InsertIdx
Iterate
Lattice
Lemmas
Lex
MinMax
Monad
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Permutation
Pi
Prime
ProdSigma
Range
Rotate
Scan
Sort
Sublists
Sym
TFAE
TakeDrop
TakeWhile
Zip
Matrix
Basic
Basis
Block
Composition
ConjTranspose
DMatrix
Defs
Diagonal
Invertible
Kronecker
Mul
Notation
RowCol
Matroid
Minor
Restrict
Rank
Cardinal
ENat
Finite
Basic
Closure
Constructions
Dual
IndepAxioms
Init
Map
Multiset
AddSub
Antidiagonal
Basic
Bind
Count
Dedup
Defs
Filter
FinsetOps
Fintype
Fold
Lattice
MapFold
NatAntidiagonal
OrderedMonoid
Pi
Powerset
Range
Replicate
Sections
Sort
Sum
Sym
UnionInter
ZeroCons
NNRat
Defs
Lemmas
Order
NNReal
Basic
Defs
Nat
Cast
Order
Basic
Field
Ring
Basic
Commute
Defs
Field
NeZero
Prod
WithTop
Choose
Basic
Bounds
Cast
Sum
Factorial
Basic
Cast
DoubleFactorial
Factorization
Basic
Defs
Induction
GCD
Basic
BigOperators
Order
Lemmas
Prime
Basic
Defs
Infinite
Int
Basic
BinaryRec
Bits
Count
Digits
Factors
Find
Init
Lattice
Log
MaxPowDiv
ModEq
Multiplicity
Notation
Pairing
Periodic
PrimeFin
Set
Sqrt
SuccPred
Totient
WithBot
Option
Basic
Defs
NAry
Ordering
Basic
PNat
Basic
Defs
Equiv
Notation
Prod
Basic
Lex
PProd
TProd
Rat
Cast
CharZero
Defs
Lemmas
Order
BigOperators
Cardinal
Defs
Encodable
Floor
Init
Lemmas
Real
Pi
Bounds
Archimedean
Basic
Cardinality
ConjExponents
ENatENNReal
Pointwise
Sqrt
Star
Set
Finite
Basic
Lattice
Lemmas
Powerset
Range
Lattice (file)
Image
Pairwise
Basic
Lattice
List
Accumulate
Basic
BoolIndicator
BooleanAlgebra
Card
CoeSort
Constructions
Countable
Defs
Disjoint
Function
Functor
Image
Inclusion
Insert
List
MemPartition
Monotone
NAry
Notation
Operations
Order
Piecewise
Prod
Restrict
Semiring
Sigma
Subset
Subsingleton
SymmDiff
UnionLift
SetLike
Basic
Fintype
Setoid
Basic
Sigma
Basic
Lex
String
Defs
Sum
Basic
Order
Sym
Sym2 (file)
Init
Basic
Tree
Basic
Vector
Basic
Defs
W
Basic
Cardinal
ZMod
Aut
Basic
Defs
IntUnitsPower
QuotientGroup
QuotientRing
Bracket
Ineq
Opposite
Part
Quot
Rel
SProd
Sign
Subtype
ULift
Dynamics
Ergodic
MeasurePreserving
FixedPoints
Basic
PeriodicPts
Defs
Lemmas
Minimal
FieldTheory
Galois
Basic
GaloisClosure
Infinite
IntermediateField
Adjoin
Algebra
Basic
Defs
Algebraic
Basic
IsAlgClosed
AlgebraicClosure
Basic
Minpoly
Basic
Field
IsIntegrallyClosed
MinpolyDiv
Normal
Basic
Closure
Defs
SplittingField
Construction
IsSplittingField
Extension
Finiteness
Fixed
IsSepClosed
KrullTopology
KummerPolynomial
Perfect
PolynomialGaloisGroup
PrimitiveElement
Separable
SeparableClosure
SeparableDegree
Tower
GroupTheory
Commutator
Basic
Congruence
Basic
Defs
Hom
Opposite
Coset
Basic
Card
Defs
GroupAction
DomAct
Basic
SubMulAction (file)
Pointwise
Basic
ConjAct
Defs
FixedPoints
FixingSubgroup
Hom
IterateAct
Pointwise
Quotient
Ring
MonoidLocalization
Away
Basic
MonoidWithZero
OreLocalization
Basic
OreSet
Perm
Cycle
Basic
Factors
Type
Basic
Closure
Fin
Finite
List
Option
Sign
Support
ViaEmbedding
QuotientGroup
Basic
Defs
Finite
SpecificGroups
Cyclic
Subgroup
Center
Centralizer
Simple
Submonoid
Center
Centralizer
Subsemigroup
Center
Centralizer
Abelianization
Archimedean
Divisible
Exponent
Finiteness
Index
NoncommPiCoprod
OrderOfElement
PGroup
Rank
Solvable
Sylow
Torsion
Lean
Elab
Tactic
Basic
Term
Expr
Basic
ExtraRecognizers
Rat
ReplaceRec
Meta (file)
RefinedDiscrTree (file)
Basic
Encode
Lookup
Pi
Basic
CongrTheorems
Simp
PrettyPrinter
Delaborator
EnvExtension
Name
LinearAlgebra
AffineSpace
AffineSubspace
Basic
Defs
AffineEquiv
AffineMap
Basis
Combination
Defs
FiniteDimensional
Independent
Midpoint
Ordered
Pointwise
Restrict
Slope
Alternating
Basic
Basis
Basic
Bilinear
Cardinality
Defs
Fin
Prod
SMul
Submodule
VectorSpace
BilinearForm
Basic
DualLattice
Hom
Properties
Dimension
Basic
Constructions
DivisionRing
ErdosKaplansky
Finite
Finrank
Free
FreeAndStrongRankCondition
LinearMap
RankNullity
StrongRankCondition
Subsingleton
DirectSum
Finsupp
TensorProduct
Dual
Basis
Defs
Lemmas
FiniteDimensional
Basic
Defs
Lemmas
Finsupp
Defs
LSum
LinearCombination
Pi
Span
SumProd
Supported
VectorSpace
FreeModule
Finite
Basic
CardQuotient
Matrix
Quotient
Basic
Determinant
IdealQuotient
PID
StrongRankCondition
LinearIndependent
Basic
Defs
Lemmas
Matrix
Charpoly
Basic
Coeff
LinearMap
Minpoly
Determinant
Basic
GeneralLinearGroup
Defs
AbsoluteValue
Adjugate
Basis
BilinearForm
Block
Diagonal
MvPolynomial
Nondegenerate
NonsingularInverse
Polynomial
Reindex
SemiringInverse
SesquilinearForm
SpecialLinearGroup
StdBasis
ToLin
ToLinearEquiv
Trace
Transvection
Multilinear
Basic
Basis
Curry
Quotient
Basic
Defs
Pi
Span
Basic
Defs
TensorProduct
Associator
Basic
Basis
Quotient
RightExactness
Tower
BilinearMap
Contraction
Countable
DFinsupp
Determinant
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
LinearPMap
Orientation
Pi
Prod
Projection
Ray
SModEq
SesquilinearForm
StdBasis
Trace
UnitaryGroup
Vandermonde
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Pi
Equiv
Fin
Basic
Rotate
Basic
Defs
Embedding
Finset
Fintype
Functor
List
Multiset
Nat
Option
PartialEquiv
Prod
Set
Sum
Function
Basic
Coequalizer
CompTypeclasses
Conjugate
Defs
DependsOn
Iterate
ULift
Nontrivial
Basic
Defs
Small
Basic
Defs
List
Set
Basic
Denumerable
ExistsUnique
IsEmpty
Lemmas
Nonempty
OpClass
Pairwise
Relation
Relator
Unique
UnivLE
MeasureTheory
Constructions
BorelSpace
Basic
Complex
ContinuousLinearMap
Metric
Metrizable
Order
Real
Polish
Basic
HaarToSphere
Pi
Covering
Besicovitch
BesicovitchVectorSpace
Differentiation
VitaliFamily
Function
L1Space
AEEqFun
HasFiniteIntegral
Integrable
LpSeminorm
Basic
ChebyshevMarkov
CompareExp
Defs
TriangleInequality
LpSpace
Basic
Complete
Indicator
SpecialFunctions
Basic
StronglyMeasurable
AEStronglyMeasurable
Basic
ENNReal
Lemmas
AEEqFun
AEEqOfLIntegral
AEMeasurableOrder
AEMeasurableSequence
ConvergenceInMeasure
Egorov
EssSup
Jacobian
LocallyIntegrable
LpOrder
SimpleFunc
SimpleFuncDense
SimpleFuncDenseLp
Group
Action
Arithmetic
Defs
FundamentalDomain
GeometryOfNumbers
Integral
LIntegral
MeasurableEquiv
Measure
Pointwise
Prod
Integral
Bochner
Basic
ContinuousLinearMap
FundThmCalculus
L1
Set
VitaliCaratheodory
IntervalIntegral
Basic
FundThmCalculus
IntegrationByParts
Lebesgue
Add
Basic
Countable
DominatedConvergence
Map
Markov
MeasurePreserving
Norm
Sub
Asymptotics
Average
CircleIntegral
DivergenceTheorem
DominatedConvergence
ExpDecay
FinMeasAdditive
Gamma
IntegrableOn
IntegralEqImproper
Layercake
Marginal
MeanInequalities
Pi
Prod
SetIntegral
SetToL1
MeasurableSpace
Basic
Constructions
CountablyGenerated
Defs
Embedding
EventuallyMeasurable
Instances
MeasurablyGenerated
Pi
Prod
Measure
Decomposition
Exhaustion
Hahn
Lebesgue
Haar
Basic
InnerProductSpace
NormedSpace
OfBasis
Unique
Lebesgue
Basic
Complex
EqHaar
Integral
VolumeOfBalls
Typeclasses
Finite
NoAtoms
Probability
SFinite
AEDisjoint
AEMeasurable
AbsolutelyContinuous
Comap
Content
Count
Dirac
Doubling
EverywherePos
GiryMonad
Map
MeasureSpace
MeasureSpaceDef
MutuallySingular
NullMeasurable
OpenPos
Prod
QuasiMeasurePreserving
Real
Regular
Restrict
Stieltjes
Sub
Trim
WithDensity
Order
Lattice
OuterMeasure
AE
Basic
BorelCantelli
Caratheodory
Defs
Induced
OfFunction
Operations
PiSystem
Topology
NumberTheory
ClassNumber
AdmissibleAbs
AdmissibleAbsoluteValue
Finite
NumberField
CanonicalEmbedding
Basic
ConvexBody
Discriminant
Basic
Defs
InfinitePlace
Basic
Embeddings
TotallyRealComplex
Units
Basic
Basic
ClassNumber
Embeddings
FractionalIdeal
Norm
Padics
PadicVal
Basic
Defs
PadicIntegers
PadicNorm
PadicNumbers
ProperSpace
RingHoms
Divisors
Order
Atoms (file)
Finite
BoundedOrder
Basic
Lattice
Monotone
Bounds
Basic
Defs
Image
OrderIso
CompactlyGenerated
Basic
Intervals
CompleteLattice
Basic
Chain
Defs
Finset
Lemmas
ConditionallyCompleteLattice
Basic
Defs
Finset
Group
Indexed
Defs
LinearOrder
PartialOrder
Unbundled
Filter
AtTopBot
Archimedean
Basic
BigOperators
CompleteLattice
CountablyGenerated
Defs
Disjoint
Field
Finite
Finset
Group
Map
ModEq
Monoid
Prod
Ring
Tendsto
Bases
Basic
Finite
Germ
Basic
Ultrafilter
Basic
Defs
Basic
Cofinite
CountableInter
CountableSeparatingOn
CountablyGenerated
Curry
Defs
ENNReal
EventuallyConst
Extr
Finite
IndicatorFunction
Interval
IsBounded
Ker
Lift
Map
NAry
Pi
Pointwise
Prod
SmallSets
Subsingleton
Tendsto
Fin
Basic
Tuple
GaloisConnection
Basic
Defs
Heyting
Basic
Hom
Hom
Basic
Bounded
BoundedLattice
CompleteLattice
Lattice
Order
Set
WithTopBot
Interval
Finset
Basic
Defs
Fin
Nat
SuccPred
Set
Basic
Defs
Disjoint
Fin
Image
Infinite
LinearOrder
Monotone
OrdConnected
OrdConnectedComponent
OrderEmbedding
OrderIso
Pi
ProjIcc
SuccPred
UnorderedInterval
WithBotTop
Multiset
Monotone
Basic
Defs
Monovary
Odd
Union
Preorder
Chain
RelIso
Basic
Set
SuccPred
Archimedean
Basic
CompleteLinearOrder
InitialSeg
Limit
LinearLocallyFinite
Relation
WithBot
UpperLower
Basic
Closure
CompleteLattice
Fibration
Principal
Antichain
Antisymmetrization
Basic
BooleanAlgebra
BooleanSubalgebra
Circular
Closure
Cofinal
Compare
CompleteBooleanAlgebra
CompleteLatticeIntervals
Copy
Cover
Directed
DirectedInverseSystem
Disjoint
Disjointed
FixedPoints
GameAdd
Ideal
InitialSeg
Iterate
JordanHolder
KrullDimension
Lattice
LatticeIntervals
LiminfLimsup
Max
MinMax
Minimal
ModularLattice
Nat
Notation
OmegaCompletePartialOrder
OrdContinuous
OrderIsoNat
Part
PartialSups
PiLex
PropInstances
RelClasses
RelSeries
ScottContinuity
SetNotation
Sublattice
SupClosed
SupIndep
SymmDiff
Synonym
TypeTags
ULift
WellFounded
WellFoundedSet
WellQuasiOrder
WithBot
Zorn
ZornAtoms
Probability
ConditionalProbability
UniformOn
RingTheory
AdicCompletion
Basic
LocalRing
Adjoin
Basic
Dimension
FG
Field
Polynomial
Tower
Algebraic
Basic
Defs
Integral
MvPolynomial
AlgebraicIndependent
Adjoin
Basic
Defs
TranscendenceBasis
Transcendental
Artinian
Module
Ring
Congruence
Basic
Defs
Opposite
Coprime
Basic
Ideal
Lemmas
DedekindDomain
Basic
Dvr
Factorization
Ideal
IntegralClosure
PID
DiscreteValuationRing
Basic
TFAE
Finiteness
Basic
Bilinear
Cardinality
Defs
Finsupp
Ideal
Nakayama
Prod
Projective
Subalgebra
FractionalIdeal
Basic
Norm
Operations
Ideal
AssociatedPrime
Basic
Finiteness
MinimalPrime
Basic
Localization
Norm
AbsNorm
Quotient
Basic
Defs
Index
Noetherian
Operations
PowTransition
Basic
Basis
BigOperators
Colon
Cotangent
Defs
GoingUp
Height
IsPrimary
IsPrincipal
Lattice
Maps
Maximal
Nonunits
Operations
Over
Pointwise
Prime
Prod
Span
Int
Basic
IntegralClosure
Algebra
Basic
Defs
IsIntegral
Basic
Defs
IsIntegralClosure
Basic
Defs
IntegrallyClosed
Jacobson
Ideal
Radical
Semiprimary
KrullDimension
Basic
LocalProperties
Basic
IntegrallyClosed
Submodule
LocalRing
MaximalIdeal
Basic
Defs
ResidueField
Basic
Defs
RingHom
Basic
Basic
Defs
Quotient
Localization
Away
Basic
Algebra
AsSubring
AtPrime
BaseChange
Basic
Defs
Finiteness
FractionRing
Ideal
Integer
Integral
LocalizationLocalization
Module
NormTrace
NumDen
Submodule
MvPolynomial
Symmetric
Defs
Basic
Tower
MvPowerSeries
Basic
Inverse
LexOrder
NoZeroDivisors
Nilpotent
Basic
Defs
Lemmas
Noetherian
Basic
Defs
Nilpotent
Orzech
UniqueFactorizationDomain
NonUnitalSubring
Basic
Defs
NonUnitalSubsemiring
Basic
Defs
Norm
Basic
Defs
Transitivity
OreLocalization
Basic
Ring
Polynomial
Eisenstein
Basic
Criterion
Distinguished
Basic
Content
GaussLemma
Ideal
IntegralNormalization
Nilpotent
Pochhammer
Quotient
RationalRoot
ScaleRoots
SeparableDegree
Tower
UniqueFactorization
Vieta
PowerSeries
Basic
Inverse
NoZeroDivisors
Order
Trunc
RingHom
Finite
RootsOfUnity
Basic
PrimitiveRoots
SimpleModule
Basic
SimpleRing
Basic
Defs
Spectrum
Maximal
Basic
Defs
Localization
Prime
Basic
Defs
Noetherian
RingHom
Topology
TensorProduct
Basic
Finite
Free
Trace
Basic
Defs
TwoSidedIdeal
Basic
Kernel
Lattice
Operations
UniqueFactorizationDomain
Basic
Defs
FactorSet
Finite
GCDMonoid
Ideal
Multiplicative
Multiplicity
NormalizedFactors
Valuation
Basic
Integers
PrimeMultiplicity
ValuationRing
AdjoinRoot
AlgebraTower
Bezout
ChainOfDivisors
ClassGroup
Discriminant
EuclideanDomain
Filtration
FiniteLength
FinitePresentation
FiniteType
HopkinsLevitzki
IntegralDomain
IsPrimary
IsTensorProduct
Length
MatrixAlgebra
MatrixPolynomialAlgebra
Multiplicity
Nakayama
OrzechProperty
PolynomialAlgebra
PowerBasis
PrincipalIdealDomain
ReesAlgebra
RingHomProperties
Support
ZMod
SetTheory
Cardinal
Aleph
Arithmetic
Basic
Cofinality
Continuum
Defs
ENat
Finite
Finsupp
Order
Pigeonhole
Regular
SchroederBernstein
Subfield
ToNat
UnivLE
Ordinal
Arithmetic
Basic
Enum
Exponential
Family
FixedPoint
Tactic
Attr
Core
Register
Bound
Attribute
Init
CC (file)
Addition
Datatypes
Lemmas
MkProof
CancelDenoms
Core
CategoryTheory
CheckCompositions
Elementwise
Reassoc
Slice
Continuity (file)
Init
Finiteness (file)
Attr
FunProp (file)
Attr
Core
Decl
Elab
FunctionData
Mor
StateList
Theorems
ToBatteries
Types
GCongr (file)
Core
CoreAttrs
ForwardAttr
Linarith (file)
Oracle
SimplexAlgorithm (file)
Datatypes
Gauss
PositiveVector
SimplexAlgorithm
Datatypes
Frontend
Lemmas
Parsing
Preprocessing
Verification
LinearCombination (file)
Lemmas
Linter (file)
DeprecatedModule
DeprecatedSyntaxLinter
DirectoryDependency
DocPrime
DocString
FlexibleLinter
GlobalAttributeIn
HashCommandLinter
HaveLetLinter
Header
Lint
MinImports
Multigoal
OldObtain
PPRoundtrip
Style
UnusedTactic
UnusedTacticExtension
UpstreamableDecl
Measurability (file)
Init
Monotonicity
Attr
Basic
Nontriviality (file)
Core
NormNum (file)
Basic
Core
DivMod
Eq
GCD
Ineq
Inv
OfScientific
Pow
Result
Order (file)
Graph
Basic
Tarjan
CollectFacts
Preprocessing
Positivity (file)
Basic
Core
Finset
Relation
Rfl
Symm
Ring (file)
Basic
Compare
PNat
RingNF
Simproc
ExistsAndEq
Simps
Basic
NotationClass
ToAdditive (file)
Frontend
Widget
Calc
CongrM
Conv
SelectInsertParamsClass
SelectPanelUtils
Abel
AdaptationNote
Algebraize
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Basic
ByContra
Cases
CasesM
Check
Choose
ClearExcept
ClearExclamation
Clear_
Coe
Common
ComputeDegree
CongrExclamation
CongrM
Constructor
ContinuousFunctionalCalculus
Contrapose
Conv
Convert
Core
DeclarationNames
DefEqTransformations
DeprecateTo
DeriveFintype
Eqns
ErwQuestion
ExistsI
ExtendDoc
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FastInstance
FieldSimp
FinCases
Find
Generalize
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
HaveI
HigherOrder
Hint
InferParam
Inhabit
IntervalCases
IrreducibleDef
Lemma
Lift
MinImports
MkIffOfInductiveProp
Module
MoveAdd
NoncommRing
NthRewrite
Observe
OfNat
PPWithUniv
Peel
Propose
ProxyType
Push
Qify
RSuffices
Recover
Rename
RenameBVar
Rify
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SplitIfs
Spread
StacksAttribute
Subsingleton
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TautoSet
TermCongr
ToExpr
ToLevel
Trace
TryThis
TypeCheck
TypeStar
UnsetOption
Use
Variable
WLOG
WithoutCDot
Zify
Topology
Algebra
Group
Basic
ClosedSubgroup
Compact
Defs
GroupTopology
Pointwise
Quotient
InfiniteSum
Basic
Constructions
Defs
ENNReal
Field
Group
Module
NatInt
Order
Real
Ring
IsUniformGroup
Basic
Defs
Module
Multilinear
Basic
Bounded
Topology
Basic
Compact
Determinant
Equiv
FiniteDimension
LinearMap
LinearMapPiProd
LocallyConvex
Simple
Star
StrongTopology
UniformConvergence
WeakBilin
Monoid (file)
Defs
Order
Archimedean
Field
Group
LiminfLimsup
Ring
Basic
Compact
Ideal
Real
SeparationQuotient
Basic
Section
Affine
Algebra
ClosedSubgroup
ConstMulAction
Constructions
ContinuousMonoidHom
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Indicator
MulAction
OpenSubgroup
Polynomial
Star
Support
UniformConvergence
UniformField
UniformMulAction
UniformRing
Baire
CompleteMetrizable
Lemmas
Bornology
Absorbs
Basic
BoundedOperation
Constructions
Hom
Real
Compactness
Bases
Compact
Lindelof
LocallyCompact
LocallyFinite
SigmaCompact
Connected
Basic
Clopen
LocPathConnected
LocallyConnected
PathConnected
TotallyDisconnected
Constructions (file)
SumProd
ContinuousMap
Bounded
Basic
Normed
Star
Algebra
Basic
CocompactMap
Compact
ContinuousMapZero
Defs
Ordered
Star
Defs
Basic
Filter
Induced
Sequences
Ultrafilter
EMetricSpace
Basic
Defs
Diam
Lipschitz
Pi
FiberBundle
IsHomeomorphicTrivialBundle
GDelta
Basic
MetrizableSpace
UniformSpace
Hom
ContinuousEval
ContinuousEvalConst
Homeomorph
Defs
Lemmas
Instances
ENNReal
Lemmas
EReal
Lemmas
NNReal
Lemmas
Real
Lemmas
AddCircle
Complex
Discrete
Int
Matrix
Nat
Rat
RealVectorSpace
Sign
ZMultiples
LocallyConstant
Basic
Maps
Proper
Basic
Basic
OpenQuotient
MetricSpace
ProperSpace (file)
Real
Pseudo
Basic
Constructions
Defs
Lemmas
Pi
Real
Ultra
Basic
Algebra
Antilipschitz
Basic
Bounded
CantorScheme
CauSeqFilter
Cauchy
Completion
Defs
Dilation
DilationEquiv
Equicontinuity
Gluing
HausdorffDistance
IsometricSMul
Isometry
Lipschitz
Perfect
PiNat
Polish
ThickenedIndicator
Thickening
Metrizable
Basic
CompletelyMetrizable
Real
Uniformity
Urysohn
Order (file)
Basic
Bornology
Compact
DenselyOrdered
ExtendFrom
IntermediateValue
IsLUB
Lattice
LeftRight
LeftRightLim
LeftRightNhds
LocalExtr
Monotone
MonotoneContinuity
MonotoneConvergence
OrderClosed
ProjIcc
Real
Rolle
T5
Separation
Basic
CountableSeparatingOn
GDelta
Hausdorff
Regular
SeparatedNhds
Sets
Closeds
Compacts
OpenCover
Opens
Spectral
Basic
Hom
Prespectral
UniformSpace
AbstractCompletion
Basic
Cauchy
Compact
CompactConvergence
CompleteSeparated
Completion
Defs
Equicontinuity
Equiv
HeineCantor
LocallyUniformConvergence
OfFun
Pi
Real
Separation
UniformApproximation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
Bases
Basic
Clopen
Closure
ClusterPt
Coherent
CompactOpen
Constructible
Continuous
ContinuousOn
DenseEmbedding
DiscreteSubset
ExtendFrom
Filter
IndicatorConstPointwise
Inseparable
Irreducible
IsLocalHomeomorph
KrullDimension
LocalAtTarget
LocallyClosed
LocallyFinite
Neighborhoods
NhdsSet
NoetherianSpace
PartialHomeomorph
Path
Perfect
Piecewise
QuasiSeparated
Semicontinuous
SeparatedMap
Sequences
Sober
Ultrafilter
UnitInterval
UrysohnsLemma
Util
AddRelatedDecl
AssertExists
AssertExistsExt
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
MemoFix
Notation3
PPOptions
Qq
Superscript
SynthesizeUsing
Tactic
TermReduce
TransImports
WhatsNew
WithWeakNamespace
Init
Plausible (file)
Attr
Functions
Gen
Random
Sampleable
Tactic
Testable
ProofWidgets
Component
Basic
MakeEditLink
OfRpcMethod
Data
Html
Cancellable
Compat
Util
Qq (file)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
Simp
SortLocalDecls
Typ
Std (file)
Classes (file)
Ord
Data (file)
DHashMap (file)
Internal
AssocList
Basic
Lemmas
Defs
HashesTo
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
Lemmas
Raw
RawDef
RawLemmas
DTreeMap (file)
Internal
WF
Defs
Lemmas
Balanced
Balancing
Cell
Def
Lemmas
Model
Operations
Ordered
Queries
Raw (file)
AdditionalOperations
Basic
Lemmas
WF
AdditionalOperations
Basic
Lemmas
ExtDHashMap (file)
Basic
Lemmas
ExtHashMap (file)
Basic
Lemmas
ExtHashSet (file)
Basic
Lemmas
HashMap (file)
AdditionalOperations
Basic
Lemmas
Raw
RawLemmas
HashSet (file)
Basic
Lemmas
Raw
RawLemmas
Internal
List
Associative
Defs
Cut
TreeMap (file)
Raw (file)
AdditionalOperations
Basic
Lemmas
WF
AdditionalOperations
Basic
Lemmas
TreeSet (file)
Raw (file)
Basic
Lemmas
WF
AdditionalOperations
Basic
Lemmas
Internal (file)
Async (file)
Basic
Select
TCP
Timer
UDP
Parsec (file)
Basic
ByteArray
String
UV (file)
Loop
TCP
Timer
UDP
Rat
Net (file)
Addr
Sat (file)
AIG (file)
RefVecOperator (file)
Fold
Map
Zip
Basic
CNF
Cached
CachedGates
CachedGatesLemmas
CachedLemmas
If
LawfulOperator
LawfulVecOperator
Lemmas
RefVec
Relabel
RelabelNat
CNF (file)
Basic
Dimacs
Literal
Relabel
RelabelFin
Sync (file)
Barrier
Basic
Channel
Mutex
RecursiveMutex
SharedMutex
Tactic (file)
BVDecide (file)
Bitblast (file)
BVExpr (file)
Circuit (file)
Impl (file)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Neg
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Sub
Udiv
Ult
Umod
ZeroExtend
Carry
Const
Expr
Pred
Substructure
Var
Lemmas (file)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Neg
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Sub
Udiv
Ult
Umod
ZeroExtend
Basic
Carry
Const
Expr
Pred
Var
Basic
BoolExpr (file)
Basic
Circuit
LRAT (file)
Internal
Formula (file)
Class
Implementation
Instance
Lemmas
RatAddResult
RatAddSound
RupAddResult
RupAddSound
Actions
Assignment
CNF
Clause
Convert
Entails
LRATChecker
LRATCheckerSound
PosFin
Actions
Checker
Parser
Normalize (file)
BitVec
Bool
Canonicalize
Equal
Prop
Reflect
Syntax
Time (file)
Date (file)
Unit
Basic
Day
Month
Week
Weekday
Year
Basic
PlainDate
ValidDate
DateTime (file)
PlainDateTime
Timestamp
Format (file)
Basic
Internal (file)
Bounded
UnitVal
Notation (file)
Spec
Time (file)
Unit
Basic
Hour
Millisecond
Minute
Nanosecond
Second
Basic
HourMarker
PlainTime
Zoned (file)
Database (file)
Basic
TZdb
TzIf
Windows
DateTime
Offset
TimeZone
ZoneRules
ZonedDateTime
Duration
references (file)

Color scheme