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
Frontend
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
FVarIdSubst
GoalDiff
Preprocess
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
)
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
Classes
Order
RatCast
SatisfiesM
CodeAction (
file
)
Attr
Basic
Deprecated
Misc
Control
ForInStep
Basic
Lemmas
Nondet
Basic
Data
Array
Init
Lemmas
Basic
Match
Merge
Monadic
BinomialHeap
Basic
Fin
Basic
Lemmas
HashMap
Basic
List
Init
Lemmas
Basic
Count
Lemmas
OfFn
Pairwise
Perm
MLList
Basic
Heartbeats
Nat
Basic
Gcd
RBMap
Alter
Basic
WF
Rat
Basic
Lemmas
String
Basic
Matcher
Sum
Basic
Lemmas
AssocList
Lean
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
UnusedNames
AttributeExtra
Except
Expr
Float
HashMap
HashSet
MonadBacktrack
NameMap
NameMapAttribute
PersistentHashMap
PersistentHashSet
Position
Syntax
TagAttribute
Linter (
file
)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Lint (
file
)
Basic
Frontend
Misc
Simp
TypeClass
Alias
Basic
Classical
Congr
Exact
Init
OpenPrivate
PermuteGoals
SeqFocus
Unreachable
Where
Util
Cache
ExtendedBinder
LibraryNote
ProofWanted
Logic
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
Attach
Basic
BasicAux
BinSearch
Bootstrap
DecidableEq
GetLit
InsertionSort
Lemmas
Mem
QSort
TakeDrop
BitVec (
file
)
Basic
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
)
Lemmas
Basic
DivMod
DivModLemmas
Gcd
Lemmas
LemmasAux
Order
Pow
List (
file
)
Nat (
file
)
Basic
Count
Erase
Find
Pairwise
Range
Sublist
TakeDrop
Sort (
file
)
Basic
Impl
Lemmas
Attach
Basic
BasicAux
Control
Count
Erase
Find
Impl
Lemmas
MinMax
Monadic
Notation
Pairwise
Perm
Range
Sublist
TakeDrop
Zip
Nat (
file
)
Bitwise (
file
)
Basic
Lemmas
Basic
Compare
Control
Div
Dvd
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Power2
SOM
Simproc
Option (
file
)
Attach
Basic
BasicAux
Instances
Lemmas
List
String (
file
)
Basic
Extra
Lemmas
ToString (
file
)
Basic
Macro
UInt (
file
)
Basic
Bitwise
Lemmas
Log2
AC
BEq
Basic
Bool
Cast
Channel
Float
Hashable
NeZero
OfScientific
Ord
PLift
Prod
Queue
Random
Range
Repr
Stream
Subtype
Sum
ULift
Zero
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
Reservoir
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
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RBMap
RBTree
Rat
SMap
SSet
Trie
DocString (
file
)
Extension
Elab (
file
)
Deriving (
file
)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
TypeName
Util
InfoTree (
file
)
Main
Types
PreDefinition (
file
)
Nonrec
Eqns
Structural (
file
)
BRecOn
Basic
Eqns
FindRecArg
IndGroupInfo
IndPred
Main
Preprocess
RecArgInfo
SmartUnfolding
WF (
file
)
Basic
Eqns
Fix
GuessLex
Ite
Main
PackMutual
Preprocess
Rel
Basic
EqUnfold
Eqns
Main
MkInhabitant
TerminationArgument
TerminationHint
Quotation (
file
)
Precheck
Util
Tactic (
file
)
BVDecide (
file
)
Frontend (
file
)
BVDecide (
file
)
Reflect
ReifiedBVExpr
ReifiedBVLogical
ReifiedBVPred
SatAtBVLogical
Attr
BVCheck
BVTrace
LRAT
Normalize
LRAT (
file
)
Trim
External
Conv (
file
)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Omega (
file
)
Core
Frontend
MinNatAbs
OmegaM
Basic
BoolToPropSimps
BuiltinTactic
Cache
Calc
Change
Config
Congr
Delta
DiscrTreeKey
Doc
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
Time
Util
Language
Lean (
file
)
Types
Basic
Linter (
file
)
Basic
Builtin
ConstructorAsVariable
Deprecated
MissingDocs
Omit
UnusedVariables
Util
Meta (
file
)
ArgsPacker (
file
)
Basic
Constructions (
file
)
BRecOn
CasesOn
NoConfusion
RecOn
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
)
Array
BitVec
Char
Core
Fin
Int
List
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
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
PProdN
RecursorInfo
Reduce
ReduceEval
SizeOf
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (
file
)
Tactic (
file
)
Doc
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
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
)
CollectAxioms
CollectFVars
CollectLevelMVars
CollectLevelParams
CollectMVars
Diff
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
TestExtern
Trace
Widget (
file
)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
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
LeanSearchClient (
file
)
Basic
LoogleSyntax
Syntax
Mathlib
Algebra
Algebra
Subalgebra
Basic
Directed
Operations
Pointwise
Prod
Tower
Basic
Bilinear
Defs
Equiv
Field
Hom
NonUnitalHom
NonUnitalSubalgebra
Operations
Opposite
Pi
Prod
Rat
RestrictScalars
Spectrum
Tower
ZMod
Associated
Basic
BigOperators
Group
Finset
List
Multiset
GroupWithZero
Action
Finset
Ring (
file
)
List
Multiset
Associated
Expect
Fin
Finprod
Finsupp
Intervals
Module
NatAntidiagonal
Option
Pi
RingEquiv
WithTop
CharP
Algebra
Basic
CharAndCard
Defs
ExpChar
Invertible
Reduced
Two
CharZero
Defs
Lemmas
Quotient
DirectSum
Basic
Decomposition
Finsupp
Module
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Field
Int
Field
Basic
Defs
Equiv
IsField
Opposite
Rat
Subfield
FreeMonoid
Basic
GCDMonoid
Basic
Finset
IntegrallyClosed
Multiset
Nat
Group
Action
Basic
Defs
Opposite
Pi
Prod
Units
Commute
Basic
Defs
Hom
Units
Equiv
Basic
TypeTags
Fin
Basic
Tuple
Hom
Basic
CompTypeclasses
Defs
End
Instances
Invertible
Basic
Defs
Pi
Basic
Lemmas
Pointwise
Finset
Basic
Set (
file
)
Basic
Semiconj
Basic
Defs
Units
Subgroup
Actions
Basic
Finite
MulOpposite
Order
Pointwise
ZPowers
Submonoid
Basic
DistribMulAction
Membership
MulOpposite
Operations
Pointwise
Subsemigroup
Basic
Membership
Operations
UniqueProds
Basic
Units (
file
)
Equiv
Hom
WithOne
Defs
AddChar
Aut
Basic
Center
Commutator
Conj
Defs
Embedding
Even
FiniteSupport
Indicator
InjSurj
Int
Nat
NatPowAssoc
Opposite
Prod
Support
TypeTags
ULift
ZeroOne
GroupPower
IterateHom
GroupWithZero
Action
Basic
Defs
Opposite
Pi
Prod
Units
Units
Basic
Equiv
Lemmas
Basic
Center
Commute
Defs
Divisibility
Hom
Indicator
InjSurj
Invertible
NeZero
NonZeroDivisors
Opposite
Pi
Prod
Semiconj
ULift
WithZero
Module
Equiv
Basic
Defs
LinearMap
Basic
Defs
End
Prod
Star
Submodule
Basic
Bilinear
EqLocus
Equiv
IterateMapComap
Ker
Lattice
LinearMap
Map
Pointwise
Range
RestrictScalars
Basic
BigOperators
Defs
Hom
LocalizedModule
MinimalAxioms
Opposites
Pi
Prod
Rat
Torsion
ULift
ZMod
MonoidAlgebra
Basic
Defs
Degree
Division
NoZeroDivisors
Support
MvPolynomial
Basic
CommRing
Degrees
Equiv
Rename
Variables
Order
Antidiag
Prod
Archimedean
Basic
BigOperators
Group
Finset
List
Multiset
Ring
Finset
List
Multiset
Expect
CauSeq
Basic
BigOperators
Completion
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Power
Rat
Group
Pointwise
Bounds
Unbundled
Abs
Basic
Int
Abs
Action
Basic
Defs
Indicator
InjSurj
Instances
Lattice
MinMax
Nat
OrderIso
PiLex
PosPart
Synonym
TypeTags
Units
GroupWithZero
Action
Synonym
Unbundled (
file
)
Lemmas
Canonical
Submonoid
Synonym
Hom
Basic
Monoid
Ring
Interval
Set
Group
Instances
Monoid
Finset
Module
Algebra
Defs
OrderedSMul
Pointwise
Rat
Synonym
Monoid
Canonical
Defs
Unbundled
Basic
Defs
ExistsOfLE
MinMax
OrderDual
Pow
WithTop
Basic
Defs
NatCast
OrderDual
Prod
TypeTags
Units
WithTop
Nonneg
Field
Floor
Ring
Positive
Ring
Ring
Unbundled
Basic
Nonneg
Rat
Abs
Basic
Canonical
Cast
Defs
Finset
InjSurj
Int
Nat
Pow
Rat
Synonym
WithTop
Star
Basic
Sub
Unbundled
Basic
Basic
Defs
WithTop
AbsoluteValue
AddGroupWithTop
Floor
Invertible
Kleene
Monovary
Pi
SuccPred
ToIntervalMod
ZeroLEOne
PUnitInstances
Algebra
Module
Polynomial
Degree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
BigOperators
CancelLeads
Coeff
Derivative
Div
EraseLead
Eval
Expand
FieldDivision
GroupRingAction
Identities
Induction
Inductions
Laurent
Lifts
Monic
Monomial
Reverse
RingDivision
Roots
Splits
Regular
Basic
Pow
SMul
Ring
Action
Basic
Field
Group
Invariant
Subobjects
Divisibility
Basic
Hom
Basic
Defs
Pointwise
Set
Subring
Basic
Pointwise
Units
Subsemiring
Basic
Pointwise
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
Pi
Pointwise
Prod
Rat
SelfAdjoint
StarAlgHom
StarRingHom
Subalgebra
Unitary
AddTorsor
DirectLimit
Exact
FreeAlgebra
GeomSum
IsPrimePow
ModEq
NeZero
Opposites
Periodic
QuadraticDiscriminant
Quotient
SMulWithZero
Analysis
Analytic
Basic
CPolynomial
ChangeOrigin
Composition
Constructions
Inverse
Linear
Uniqueness
Within
Asymptotics
AsymptoticEquivalent
Asymptotics
Theta
BoxIntegral
Box
Basic
SubboxInduction
Partition
Additive
Basic
Filter
Measure
Split
SubboxInduction
Tagged
Basic
DivergenceTheorem
Integrability
CStarAlgebra
Basic
Calculus
Conformal
NormedSpace
ContDiff
Basic
Defs
FTaylorSeries
RCLike
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
Mul
Polynomial
Pow
Shift
Slope
ZPow
FDeriv
Add
Analytic
Basic
Bilinear
Comp
Equiv
Linear
Measurable
Mul
Pi
Prod
RestrictScalars
IteratedDeriv
Defs
Lemmas
LocalExtr
Basic
Rolle
DiffContOnCl
Dslope
FormalMultilinearSeries
LogDeriv
MeanValue
TangentCone
Complex
Polynomial
Basic
Arg
Asymptotics
Basic
CauchyIntegral
Circle
Conformal
Isometry
Liouville
ReImTopology
RealDeriv
Convex
Cone
Basic
Extension
SpecificFunctions
Basic
Basic
Between
Combination
Function
Gauge
Hull
Jensen
Mul
Normed
Segment
Slope
Star
Strict
StrictConvexSpace
Topology
Uniform
InnerProductSpace
Basic
GramSchmidtOrtho
Orientation
Orthogonal
PiL2
Projection
Symmetric
LocallyConvex
BalancedCoreHull
Basic
Bounded
Polar
WithSeminorms
Normed
Affine
AddTorsor
AddTorsorBases
Isometry
Algebra
Exponential
Field
Basic
InfiniteSum
Lemmas
UnitBall
Group
AddCircle
AddTorsor
BallSphere
Basic
Bounded
Completion
Constructions
Hom
InfiniteSum
Int
Lemmas
Pointwise
Quotient
Rat
Seminorm
Submodule
Uniform
Lp
PiLp
WithLp
Module
Basic
Completion
Dual
FiniteDimension
Ray
Span
Operator
Banach
BoundedLinearMaps
ContinuousLinearMap
LinearIsometry
Order
Basic
Lattice
Ring
Units
MulAction
NormedSpace
HahnBanach
Extension
SeparatingDual
Separation
Multilinear
Basic
Curry
OperatorNorm
Asymptotics
Basic
Bilinear
Completeness
Mul
NNNorm
NormedSpace
ConformalLinearMap
Extend
IndicatorFunction
Pointwise
RCLike
Real
RieszLemma
RCLike
Basic
Lemmas
SpecialFunctions
Complex
Arg
Log
Log
Base
Basic
Deriv
Pow
Asymptotics
Complex
Continuity
NNReal
Real
Trigonometric
Angle
Basic
Inverse
Exp
ExpDeriv
Exponential
NonIntegrable
SpecificLimits
Basic
Normed
MeanInequalities
MeanInequalitiesPow
Oscillation
Seminorm
CategoryTheory
Adjunction
Basic
FullyFaithful
Bicategory
Functor
Lax
Oplax
Prelax
Pseudofunctor
Basic
Coherence
Free
LocallyDiscrete
Strict
Category
Basic
Cat
Init
Comma
Arrow
Basic
ConcreteCategory
Basic
Bundled
Functor
Basic
Category
Const
FullyFaithful
Hom
Trifunctor
Monoidal
Free
Basic
Coherence
Category
Functor
MorphismProperty
Basic
Pi
Basic
Products
Basic
Unitor
DiscreteCategory
EpiMono
EqToHom
Equivalence
EssentialImage
FullSubcategory
Groupoid
Iso
NatIso
NatTrans
Opposites
PathCategory
Quotient
Types
Whiskering
Yoneda
Combinatorics
Enumerative
Catalan
Composition
Partition
Quiver
Basic
Path
Push
Symmetric
Control
Monad
Basic
Cont
Writer
Traversable
Basic
Lemmas
Applicative
Basic
Bifunctor
Combinators
EquivFunctor
Functor
Lawful
Random
ULift
ULiftable
Data
Array
Defs
Bool
Basic
Set
Complex
Abs
Basic
BigOperators
Cardinality
Exponential
FiniteDimensional
Module
Order
Countable
Basic
Defs
DFinsupp
Basic
Encodable
Lex
NeLocus
Order
ENNReal
Basic
Inv
Operations
Real
ENat
Basic
Lattice
Fin
Tuple
Basic
Basic
VecNotation
Finite
Basic
Card
Defs
Set
Finset
Attr
Basic
Card
Density
Fin
Fold
Image
Lattice
Max
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
Piecewise
Powerset
Preimage
Prod
Sigma
Sort
Sum
Sym
Union
Update
Finsupp
Antidiagonal
Basic
Defs
Encodable
Fin
Fintype
Indicator
Lex
Multiset
Order
ToDFinsupp
Fintype
Basic
BigOperators
Card
CardEmbedding
Fin
Lattice
List
Option
Order
Parity
Perm
Pi
Powerset
Prod
Quotient
Sigma
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Order
Basic
Lemmas
Units
Bitwise
CharZero
ConditionallyCompleteOrder
Defs
DivMod
GCD
Interval
LeastGreatest
Lemmas
Log
ModEq
Notation
Range
Sqrt
SuccPred
List
EditDistance
Bounds
Defs
Estimator
Basic
Chain
Count
Cycle
Dedup
Defs
Duplicate
FinRange
Forall2
GetD
Indexes
Infix
InsertNth
Join
Lattice
Lex
MinMax
Monad
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
ProdSigma
Range
Rotate
Sort
Sublists
Sym
TFAE
Zip
MLList
BestFirst
Matrix
Basic
Basis
Block
DMatrix
Invertible
Notation
RowCol
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
NatAntidiagonal
Nodup
OrderedMonoid
Pi
Powerset
Range
Sections
Sort
Sum
Sym
NNRat
Defs
Lemmas
Order
NNReal
Basic
Star
Nat
Cast
Order
Basic
Field
Ring
Basic
Commute
Defs
Field
NeZero
Prod
WithTop
Choose
Basic
Bounds
Cast
Central
Sum
Factorial
Basic
Cast
Factorization
Basic
Defs
Induction
PrimePow
Fib
Basic
GCD
Basic
BigOperators
Order
Lemmas
Prime
Basic
Defs
Bits
Bitwise
Count
Defs
Digits
Factors
Find
Lattice
Log
MaxPowDiv
ModEq
Multiplicity
Notation
Pairing
PartENat
Periodic
PrimeFin
Set
Size
Sqrt
Squarefree
SuccPred
Totient
WithBot
Option
Basic
Defs
NAry
Ordering
Basic
PNat
Basic
Defs
Equiv
Prime
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
BigOperators
Finite
Interval
ListOfFn
SMul
Accumulate
Basic
BoolIndicator
Constructions
Countable
Defs
Finite
Function
Functor
Image
Lattice
List
MemPartition
Monotone
NAry
Notation
Operations
Prod
Semiring
Sigma
Subset
Subsingleton
UnionLift
SetLike
Basic
Setoid
Basic
Sigma
Basic
Lex
String
Defs
Sum
Basic
Order
Sym
Sym2 (
file
)
Init
Order
Basic
Tree
Basic
Vector
Basic
Defs
W
Basic
Cardinal
ZMod
Algebra
Basic
Defs
IntUnitsPower
Module
Quotient
Units
Bracket
Opposite
Part
Quot
Rel
SProd
Sign
Subtype
ULift
Dynamics
Ergodic
MeasurePreserving
FixedPoints
Basic
Minimal
PeriodicPts
FieldTheory
Finite
Basic
GaloisField
Trace
Galois (
file
)
Basic
IntermediateField
Algebraic
Basic
IsAlgClosed
AlgebraicClosure
Basic
Minpoly
Basic
Field
IsIntegrallyClosed
MinpolyDiv
RatFunc
AsPolynomial
Basic
Defs
SplittingField
Construction
IsSplittingField
Adjoin
Extension
Finiteness
Fixed
Normal
NormalClosure
Perfect
PolynomialGaloisGroup
PrimitiveElement
Separable
Tower
GroupTheory
Commutator
Basic
Congruence
Basic
Opposite
Coset
Basic
Card
FreeGroup
Basic
GroupAction
DomAct
Basic
SubMulAction (
file
)
Pointwise
Basic
ConjAct
FixedPoints
FixingSubgroup
Hom
IterateAct
Pointwise
Quotient
Ring
MonoidLocalization
Basic
MonoidWithZero
Perm
Cycle
Basic
Factors
Type
Basic
Closure
Fin
Finite
List
Option
Sign
Support
ViaEmbedding
QuotientGroup
Basic
SpecificGroups
Cyclic
Subgroup
Center
Centralizer
Simple
Submonoid
Center
Centralizer
Subsemigroup
Center
Centralizer
Abelianization
Archimedean
Divisible
Exponent
Finiteness
FreeAbelianGroup
Index
OrderOfElement
PGroup
Solvable
Torsion
Init (
file
)
Algebra
Classes
Logic
Lean
Elab
Tactic
Basic
Term
Expr
Basic
ExtraRecognizers
ReplaceRec
Meta (
file
)
Basic
CongrTheorems
KAbstractPositions
Simp
PrettyPrinter
Delaborator
EnvExtension
GoalsLocation
Name
Thunk
LinearAlgebra
AffineSpace
AffineEquiv
AffineMap
AffineSubspace
Basic
Basis
Combination
FiniteDimensional
Independent
Midpoint
Pointwise
Restrict
Slope
Alternating
Basic
Basis
Basic
Bilinear
Cardinality
Defs
VectorSpace
BilinearForm
Basic
DualLattice
Hom
Properties
Dimension
Basic
Constructions
DivisionRing
Finite
Finrank
Free
FreeAndStrongRankCondition
LinearMap
RankNullity
StrongRankCondition
DirectSum
Finsupp
TensorProduct
FiniteDimensional (
file
)
Defs
FreeModule
Finite
Basic
Matrix
Basic
PID
StrongRankCondition
Matrix
Charpoly
Basic
Coeff
LinearMap
Minpoly
Determinant
Basic
GeneralLinearGroup
Basic
Defs
Adjugate
Basis
BilinearForm
Block
Diagonal
MvPolynomial
Nondegenerate
NonsingularInverse
Polynomial
Reindex
SesquilinearForm
SpecialLinearGroup
ToLin
ToLinearEquiv
Trace
Transvection
Multilinear
Basic
Basis
TensorProduct
Basic
Basis
Tower
BilinearMap
Contraction
DFinsupp
Determinant
Dual
Finsupp
FinsuppVectorSpace
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
LinearIndependent
LinearPMap
Orientation
Pi
Prod
Projection
Quotient
Ray
SModEq
SesquilinearForm
Span
StdBasis
Trace
UnitaryGroup
Vandermonde
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Basic
Defs
Embedding
Fin
Fintype
Functor
List
Nat
Option
PartialEquiv
Set
TransferInstance
Function
Basic
CompTypeclasses
Conjugate
Defs
Iterate
ULift
Nontrivial
Basic
Defs
Small
Basic
Defs
Set
Basic
Denumerable
ExistsUnique
IsEmpty
Lemmas
Nonempty
OpClass
Pairwise
Relation
Relator
Unique
MeasureTheory
Constructions
BorelSpace
Basic
Complex
ContinuousLinearMap
Metric
Metrizable
Order
Real
Prod
Basic
Integral
EventuallyMeasurable
Pi
Decomposition
Exhaustion
Function
LpSeminorm
Basic
ChebyshevMarkov
CompareExp
TriangleInequality
SpecialFunctions
Basic
StronglyMeasurable
Basic
Lemmas
AEEqFun
AEMeasurableSequence
EssSup
L1Space
LocallyIntegrable
LpOrder
LpSpace
SimpleFunc
SimpleFuncDense
SimpleFuncDenseLp
Group
Action
Arithmetic
Defs
LIntegral
MeasurableEquiv
Measure
Pointwise
Prod
Integral
Bochner
CircleIntegral
DivergenceTheorem
DominatedConvergence
FundThmCalculus
IntegrableOn
IntervalIntegral
Lebesgue
Marginal
MeanInequalities
SetIntegral
SetToL1
VitaliCaratheodory
MeasurableSpace
Basic
CountablyGenerated
Defs
Embedding
Instances
Measure
Haar
Basic
InnerProductSpace
OfBasis
Lebesgue
Basic
Complex
EqHaar
AEDisjoint
AEMeasurable
Content
Count
Dirac
Doubling
GiryMonad
MeasureSpace
MeasureSpaceDef
MutuallySingular
NullMeasurable
OpenPos
Regular
Restrict
Stieltjes
Trim
Typeclasses
WithDensity
Order
Lattice
OuterMeasure
AE
Basic
BorelCantelli
Caratheodory
Defs
Induced
OfFunction
Operations
PiSystem
NumberTheory
Cyclotomic
Basic
PrimitiveRoots
LegendreSymbol
QuadraticChar
Basic
GaussSum
AddCharacter
Basic
JacobiSymbol
QuadraticReciprocity
ZModChar
MulChar
Basic
NumberField
Basic
Padics
PadicVal
Basic
Defs
ArithmeticFunction
Divisors
GaussSum
Order
Bounds
Basic
OrderIso
CompactlyGenerated
Basic
Intervals
CompleteLattice (
file
)
Finset
ConditionallyCompleteLattice
Basic
Finset
Group
Filter
AtTopBot (
file
)
Archimedean
BigOperators
Field
Group
ModEq
Monoid
Ring
Germ
Basic
Bases
Basic
Cofinite
CountableInter
CountableSeparatingOn
Curry
ENNReal
EventuallyConst
Extr
IndicatorFunction
Interval
Ker
Lift
NAry
Pi
Pointwise
Prod
SmallSets
Subsingleton
Ultrafilter
Fin
Basic
Tuple
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
RelIso
Basic
Set
SuccPred
Archimedean
Basic
CompleteLinearOrder
Limit
Relation
UpperLower
Basic
Antichain
Antisymmetrization
Atoms
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
Compare
CompleteBooleanAlgebra
CompleteLatticeIntervals
Copy
Cover
Defs
Directed
Disjoint
Disjointed
Estimator
FixedPoints
GaloisConnection
InitialSeg
Iterate
JordanHolder
Lattice
LatticeIntervals
LiminfLimsup
Max
MinMax
Minimal
ModularLattice
Nat
Notation
OmegaCompletePartialOrder
OrderIsoNat
Part
PartialSups
PiLex
PropInstances
RelClasses
RelSeries
ScottContinuity
SetNotation
SupClosed
SupIndep
SymmDiff
Synonym
TypeTags
ULift
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
RingTheory
Adjoin
Basic
FG
Field
PowerBasis
Tower
Congruence
Basic
Opposite
Coprime
Basic
Ideal
Lemmas
DedekindDomain
AdicValuation
Basic
Ideal
IntegralClosure
FractionalIdeal
Basic
Operations
Ideal
Basic
Colon
IsPrimary
Maps
Operations
Over
Prod
Quotient
QuotientOperations
Int
Basic
IntegralClosure
Algebra
Basic
Defs
IsIntegral
Basic
Defs
IsIntegralClosure
Basic
Defs
IntegrallyClosed
LocalRing
MaximalIdeal
Basic
Defs
ResidueField
Basic
Defs
RingHom
Basic
Defs
Basic
Defs
Localization
AsSubring
AtPrime
Basic
FractionRing
Ideal
Integer
Integral
LocalizationLocalization
Module
NumDen
Submodule
MvPolynomial
Symmetric
Defs
Tower
Nilpotent
Basic
Defs
Lemmas
NonUnitalSubring
Basic
NonUnitalSubsemiring
Basic
Norm
Basic
Defs
OreLocalization
Basic
OreSet
Ring
Polynomial
Cyclotomic
Basic
Eval
Expand
Roots
Eisenstein
Basic
Basic
Content
GaussLemma
IntegralNormalization
Nilpotent
Pochhammer
Quotient
RationalRoot
ScaleRoots
Tower
Vieta
RootsOfUnity
Basic
Complex
Minpoly
TensorProduct
Basic
Trace
Basic
Defs
TwoSidedIdeal
Basic
Lattice
Operations
Valuation
Basic
ExtendToLocalization
Integers
ValuationRing
ValuationSubring
AdjoinRoot
AlgebraTower
Algebraic
Bezout
ChainOfDivisors
EisensteinCriterion
EuclideanDomain
FinitePresentation
FiniteType
Finiteness
FreeCommRing
FreeRing
IntegralDomain
JacobsonIdeal
MatrixAlgebra
MaximalSpectrum
Multiplicity
Noetherian
OrzechProperty
PolynomialAlgebra
PowerBasis
Prime
PrimeSpectrum
PrincipalIdealDomain
QuotientNoetherian
SimpleModule
UniqueFactorizationDomain
ZMod
SetTheory
Cardinal
Basic
Cofinality
Continuum
ENat
Finite
Finsupp
Ordinal
PartENat
SchroederBernstein
Subfield
ToNat
Ordinal
Arithmetic
Basic
Exponential
FixedPoint
Principal
Std
Data
HashMap
Tactic (
file
)
ArithMult (
file
)
Init
Attr
Core
Register
Bound (
file
)
Attribute
Init
CC (
file
)
Addition
Datatypes
Lemmas
CancelDenoms (
file
)
Core
CategoryTheory
Bicategory
Basic
Datatypes
Normalize
PureCoherence
Coherence (
file
)
Basic
Datatypes
Normalize
PureCoherence
Monoidal
Basic
Datatypes
Normalize
PureCoherence
BicategoricalComp
BicategoryCoherence
Elementwise
MonoidalComp
Reassoc
Slice
ToApp
Continuity (
file
)
Init
Explode (
file
)
Datatypes
Pretty
FunProp (
file
)
Attr
ContDiff
Core
Decl
Differentiable
Elab
FunctionData
Mor
RefinedDiscrTree
StateList
Theorems
ToBatteries
Types
GCongr (
file
)
Core
CoreAttrs
ForwardAttr
Linarith (
file
)
Oracle
SimplexAlgorithm (
file
)
Datatypes
Gauss
PositiveVector
SimplexAlgorithm
FourierMotzkin
Datatypes
Frontend
Lemmas
Parsing
Preprocessing
Verification
LinearCombination (
file
)
Lemmas
Linter (
file
)
AdmitLinter
DocPrime
FlexibleLinter
GlobalAttributeIn
HashCommandLinter
HaveLetLinter
Lint
MinImports
OldObtain
RefineLinter
Style
TextBased
UnusedTactic
Measurability (
file
)
Init
Monotonicity (
file
)
Attr
Basic
Lemmas
Nontriviality (
file
)
Core
NormNum (
file
)
Basic
BigOperators
Core
DivMod
Eq
GCD
Ineq
Inv
IsCoprime
LegendreSymbol
NatFib
NatSqrt
OfScientific
Pow
Prime
Result
Positivity (
file
)
Basic
Core
Finset
ReduceModChar (
file
)
Ext
Relation
Rfl
Symm
Trans
Ring (
file
)
Basic
PNat
RingNF
Sat
FromLRAT
Simps
Basic
NotationClass
ToAdditive (
file
)
Frontend
Widget
Calc
CommDiag
CongrM
Conv
GCongr
InteractiveUnfold
SelectInsertParamsClass
SelectPanelUtils
StringDiagram
Abel
AdaptationNote
Algebraize
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Basic
ByContra
Cases
CasesM
Change
Check
Choose
Clean
ClearExcept
ClearExclamation
Clear_
Coe
Common
ComputeDegree
CongrExclamation
CongrM
Constructor
ContinuousFunctionalCalculus
Contrapose
Conv
Convert
Core
DefEqTransformations
DeprecateMe
DeriveFintype
DeriveToExpr
DeriveTraversable
Eqns
Eval
ExistsI
ExtendDoc
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
Generalize
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
Have
HaveI
HelpCmd
HigherOrder
Hint
ITauto
InferParam
Inhabit
IntervalCases
IrreducibleDef
Lemma
Lift
LiftLets
LinearCombination'
MinImports
MkIffOfInductiveProp
ModCases
Module
MoveAdd
NoncommRing
NthRewrite
Observe
PPWithUniv
Peel
Polyrith
ProdAssoc
ProjectionNotation
Propose
ProxyType
PushNeg
Qify
RSuffices
Recall
Recover
Rename
RenameBVar
Replace
RewriteSearch
Rify
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SlimCheck
SplitIfs
Spread
StacksAttribute
Subsingleton
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TermCongr
ToExpr
ToLevel
Trace
TryThis
TypeCheck
TypeStar
UnsetOption
Use
Variable
WLOG
Zify
Testing
SlimCheck
Gen
Sampleable
Testable
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
WeakBilin
Nonarchimedean
Bases
Basic
Order
Archimedean
Compact
Field
Group
LiminfLimsup
Rolle
Ring
Basic
Ideal
Valued
ValuationTopology
ValuedField
Affine
Algebra
ConstMulAction
Constructions
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Monoid
MulAction
OpenSubgroup
Polynomial
Star
UniformConvergence
UniformField
UniformFilterBasis
UniformGroup
UniformMulAction
UniformRing
WithZeroTopology
Baire
CompleteMetrizable
Lemmas
Bornology
Absorbs
Basic
BoundedOperation
Constructions
Hom
Compactness
Compact
Lindelof
LocallyCompact
SigmaCompact
Connected
Basic
Clopen
LocallyConnected
PathConnected
TotallyDisconnected
ContinuousFunction
Algebra
Basic
Bounded
CocompactMap
Compact
ContinuousMapZero
Ordered
ContinuousMap
Algebra
Basic
Bounded
CocompactMap
Compact
ContinuousMapZero
Ordered
Defs
Basic
Filter
Induced
Sequences
EMetricSpace
Basic
Defs
Diam
Lipschitz
Pi
FiberBundle
IsHomeomorphicTrivialBundle
Instances
AddCircle
Discrete
ENNReal
EReal
Int
Matrix
NNReal
Nat
Rat
Real
RealVectorSpace
Sign
Maps
Proper
Basic
Basic
OpenQuotient
MetricSpace
Pseudo
Basic
Constructions
Defs
Lemmas
Pi
Real
Algebra
Antilipschitz
Basic
Bounded
CauSeqFilter
Cauchy
Completion
Defs
Dilation
DilationEquiv
Equicontinuity
HausdorffDistance
IsometricSMul
Isometry
Lipschitz
ProperSpace
ThickenedIndicator
Thickening
Metrizable
Basic
Uniformity
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
OfFun
Pi
Separation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
Bases
Basic
Clopen
CompactOpen
Constructions
ContinuousOn
DenseEmbedding
DiscreteSubset
ExtendFrom
Filter
GDelta
Homeomorph
IndicatorConstPointwise
Inseparable
Irreducible
IsLocalHomeomorph
LocallyFinite
NhdsSet
NoetherianSpace
PartialHomeomorph
QuasiSeparated
RestrictGen
Semicontinuous
SeparatedMap
Separation
Sequences
Support
UnitInterval
Util
AddRelatedDecl
AssertExists
AssertExistsExt
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
MemoFix
Notation3
Qq
SynthesizeUsing
Tactic
WhatsNew
WithWeakNamespace
ProofWidgets
Component
Panel
Basic
Basic
HtmlDisplay
MakeEditLink
OfRpcMethod
PenroseDiagram
Data
Html
Presentation
Expr
Cancellable
Compat
Util
Qq (
file
)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
SortLocalDecls
Typ
Std (
file
)
Data (
file
)
DHashMap (
file
)
Internal
AssocList
Basic
Lemmas
List
Associative
Defs
HashesTo
Pairwise
Sublist
Defs
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
Lemmas
Raw
RawDef
RawLemmas
HashMap (
file
)
AdditionalOperations
Basic
Lemmas
Raw
RawLemmas
HashSet (
file
)
Basic
Lemmas
Raw
RawLemmas
Internal (
file
)
Parsec (
file
)
Basic
ByteArray
String
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
Tactic (
file
)
BVDecide (
file
)
Bitblast (
file
)
BVExpr (
file
)
Circuit (
file
)
Impl (
file
)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Ult
ZeroExtend
Carry
Const
Expr
Pred
Var
Lemmas (
file
)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Ult
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
docs
Aesop (
file
)
Builder
Apply
Basic
Cases
Constructors
Default
Forward
NormSimp
Tactic
Unfold
BuiltinRules (
file
)
ApplyHyps
Assumption
DestructProducts
Ext
Intros
Rfl
Split
Subst
Frontend
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
FVarIdSubst
GoalDiff
Preprocess
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
)
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
Classes
Order
RatCast
SatisfiesM
CodeAction (
file
)
Attr
Basic
Deprecated
Misc
Control
ForInStep
Basic
Lemmas
Nondet
Basic
Data
Array
Init
Lemmas
Basic
Match
Merge
Monadic
BinomialHeap
Basic
Fin
Basic
Lemmas
HashMap
Basic
List
Init
Lemmas
Basic
Count
Lemmas
OfFn
Pairwise
Perm
MLList
Basic
Heartbeats
Nat
Basic
Gcd
RBMap
Alter
Basic
WF
Rat
Basic
Lemmas
String
Basic
Matcher
Sum
Basic
Lemmas
AssocList
Lean
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
UnusedNames
AttributeExtra
Except
Expr
Float
HashMap
HashSet
MonadBacktrack
NameMap
NameMapAttribute
PersistentHashMap
PersistentHashSet
Position
Syntax
TagAttribute
Linter (
file
)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Lint (
file
)
Basic
Frontend
Misc
Simp
TypeClass
Alias
Basic
Classical
Congr
Exact
Init
OpenPrivate
PermuteGoals
SeqFocus
Unreachable
Where
Util
Cache
ExtendedBinder
LibraryNote
ProofWanted
Logic
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
Attach
Basic
BasicAux
BinSearch
DecidableEq
InsertionSort
Lemmas
Mem
QSort
TakeDrop
BitVec (
file
)
Basic
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
)
Lemmas
Basic
DivMod
DivModLemmas
Gcd
Lemmas
LemmasAux
Order
Pow
List (
file
)
Nat (
file
)
Basic
Pairwise
Range
Sublist
TakeDrop
Sort (
file
)
Basic
Impl
Lemmas
Attach
Basic
BasicAux
Control
Count
Erase
Find
Impl
Lemmas
MinMax
Monadic
Notation
Pairwise
Perm
Range
Sublist
TakeDrop
Zip
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
Bitwise
Lemmas
Log2
AC
BEq
Basic
Bool
Cast
Channel
Float
Hashable
OfScientific
Ord
PLift
Prod
Queue
Random
Range
Repr
Stream
Subtype
Sum
ULift
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
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
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RBMap
RBTree
Rat
SMap
SSet
Trie
DocString (
file
)
Extension
Elab (
file
)
Deriving (
file
)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
TypeName
Util
InfoTree (
file
)
Main
Types
PreDefinition (
file
)
Nonrec
Eqns
Structural (
file
)
BRecOn
Basic
Eqns
FindRecArg
IndGroupInfo
IndPred
Main
Preprocess
RecArgInfo
SmartUnfolding
WF (
file
)
Basic
Eqns
Fix
GuessLex
Ite
Main
PackMutual
Preprocess
Rel
Basic
EqUnfold
Eqns
Main
MkInhabitant
TerminationArgument
TerminationHint
Quotation (
file
)
Precheck
Util
Tactic (
file
)
BVDecide (
file
)
Frontend (
file
)
BVDecide (
file
)
Reflect
ReifiedBVExpr
ReifiedBVLogical
ReifiedBVPred
SatAtBVLogical
Attr
BVCheck
BVTrace
LRAT
Normalize
LRAT (
file
)
Trim
External
Conv (
file
)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Omega (
file
)
Core
Frontend
MinNatAbs
OmegaM
Basic
BoolToPropSimps
BuiltinTactic
Cache
Calc
Change
Config
Congr
Delta
DiscrTreeKey
Doc
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
Time
Util
Language
Lean (
file
)
Types
Basic
Linter (
file
)
Basic
Builtin
ConstructorAsVariable
Deprecated
MissingDocs
Omit
UnusedVariables
Util
Meta (
file
)
ArgsPacker (
file
)
Basic
Constructions (
file
)
BRecOn
CasesOn
NoConfusion
RecOn
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
)
Array
BitVec
Char
Core
Fin
Int
List
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
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
PProdN
RecursorInfo
Reduce
ReduceEval
SizeOf
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (
file
)
Tactic (
file
)
Doc
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
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
)
CollectAxioms
CollectFVars
CollectLevelParams
CollectMVars
Diff
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
TestExtern
Trace
Widget (
file
)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
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
LeanSearchClient (
file
)
Basic
LoogleSyntax
Syntax
Mathlib
Algebra
Algebra
Subalgebra
Basic
Directed
Operations
Pointwise
Prod
Tower
Basic
Bilinear
Defs
Equiv
Field
Hom
NonUnitalHom
NonUnitalSubalgebra
Operations
Opposite
Pi
Prod
Rat
RestrictScalars
Spectrum
Tower
Associated
Basic
BigOperators
Group
Finset
List
Multiset
GroupWithZero
Action
Finset
Ring (
file
)
List
Multiset
Associated
Fin
Finprod
Finsupp
Intervals
Module
NatAntidiagonal
Option
Pi
RingEquiv
WithTop
CharP
Algebra
Basic
CharAndCard
Defs
ExpChar
Invertible
Reduced
Two
CharZero
Defs
Lemmas
Quotient
DirectSum
Basic
Decomposition
Finsupp
Module
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Field
Int
Field
Basic
Defs
Equiv
IsField
Opposite
Rat
Subfield
FreeMonoid
Basic
GCDMonoid
Basic
Finset
IntegrallyClosed
Multiset
Nat
Group
Action
Basic
Defs
Opposite
Pi
Prod
Units
Commute
Basic
Defs
Hom
Units
Equiv
Basic
TypeTags
Fin
Basic
Tuple
Hom
Basic
CompTypeclasses
Defs
End
Instances
Invertible
Basic
Defs
Pi
Basic
Lemmas
Pointwise
Finset
Basic
Set
Semiconj
Basic
Defs
Units
Subgroup
Actions
Basic
Finite
MulOpposite
Order
Pointwise
ZPowers
Submonoid
Basic
DistribMulAction
Membership
MulOpposite
Operations
Pointwise
Subsemigroup
Basic
Membership
Operations
UniqueProds
Basic
Units (
file
)
Equiv
Hom
WithOne
Defs
AddChar
Aut
Basic
Center
Commutator
Conj
Defs
Embedding
Even
FiniteSupport
Indicator
InjSurj
Int
Nat
NatPowAssoc
Opposite
Prod
Support
TypeTags
ULift
ZeroOne
GroupPower
IterateHom
GroupWithZero
Action
Basic
Defs
Opposite
Pi
Prod
Units
Units
Basic
Equiv
Lemmas
Basic
Center
Commute
Defs
Divisibility
Hom
Indicator
InjSurj
Invertible
NeZero
NonZeroDivisors
Opposite
Pi
Prod
Semiconj
ULift
WithZero
Module
Equiv
Basic
Defs
LinearMap
Basic
Defs
End
Prod
Star
Submodule
Basic
Bilinear
EqLocus
Equiv
IterateMapComap
Ker
Lattice
LinearMap
Map
Pointwise
Range
RestrictScalars
Basic
BigOperators
Defs
Hom
LocalizedModule
MinimalAxioms
Opposites
Pi
Prod
Rat
Torsion
ULift
MonoidAlgebra
Basic
Defs
Degree
Division
NoZeroDivisors
Support
MvPolynomial
Basic
CommRing
Degrees
Equiv
Rename
Variables
Order
Antidiag
Prod
Archimedean
Basic
BigOperators
Group
Finset
List
Multiset
Ring
Finset
List
Multiset
CauSeq
Basic
BigOperators
Completion
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Power
Rat
Group
Pointwise
Bounds
Unbundled
Abs
Basic
Int
Abs
Action
Basic
Defs
Indicator
InjSurj
Instances
Lattice
MinMax
Nat
OrderIso
PiLex
PosPart
Synonym
TypeTags
Units
GroupWithZero
Action
Synonym
Canonical
Submonoid
Synonym
Unbundled
Hom
Basic
Monoid
Ring
Interval
Set
Group
Instances
Monoid
Finset
Module
Algebra
Defs
OrderedSMul
Pointwise
Synonym
Monoid
Canonical
Defs
Unbundled
Basic
Defs
ExistsOfLE
MinMax
OrderDual
Pow
WithTop
Basic
Defs
NatCast
OrderDual
Prod
TypeTags
Units
WithTop
Nonneg
Field
Floor
Ring
Positive
Ring
Ring
Unbundled
Basic
Nonneg
Rat
Abs
Basic
Canonical
Cast
Defs
Finset
InjSurj
Int
Nat
Pow
Rat
Synonym
WithTop
Star
Basic
Sub
Unbundled
Basic
Basic
Defs
WithTop
AbsoluteValue
AddGroupWithTop
Floor
Invertible
Kleene
Monovary
Pi
SuccPred
ToIntervalMod
ZeroLEOne
PUnitInstances
Algebra
Module
Polynomial
Degree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
BigOperators
CancelLeads
Coeff
Derivative
Div
EraseLead
Eval
Expand
FieldDivision
GroupRingAction
Identities
Induction
Inductions
Laurent
Lifts
Monic
Monomial
Reverse
RingDivision
Roots
Splits
Regular
Basic
Pow
SMul
Ring
Action
Basic
Field
Group
Invariant
Subobjects
Divisibility
Basic
Hom
Basic
Defs
Pointwise
Set
Subring
Basic
Pointwise
Units
Subsemiring
Basic
Pointwise
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
Pi
Pointwise
Prod
Rat
SelfAdjoint
StarAlgHom
StarRingHom
Subalgebra
Unitary
AddTorsor
DirectLimit
Exact
FreeAlgebra
GeomSum
IsPrimePow
ModEq
NeZero
Opposites
Periodic
QuadraticDiscriminant
Quotient
SMulWithZero
Analysis
Analytic
Basic
CPolynomial
ChangeOrigin
Composition
Constructions
Linear
Uniqueness
Within
Asymptotics
AsymptoticEquivalent
Asymptotics
Theta
BoxIntegral
Box
Basic
SubboxInduction
Partition
Additive
Basic
Filter
Measure
Split
SubboxInduction
Tagged
Basic
DivergenceTheorem
Integrability
CStarAlgebra
Basic
Calculus
Conformal
NormedSpace
ContDiff
Basic
Defs
FTaylorSeries
RCLike
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
Mul
Polynomial
Pow
Shift
Slope
ZPow
FDeriv
Add
Analytic
Basic
Bilinear
Comp
Equiv
Linear
Measurable
Mul
Pi
Prod
RestrictScalars
IteratedDeriv
Defs
Lemmas
LocalExtr
Basic
Rolle
DiffContOnCl
Dslope
FormalMultilinearSeries
LogDeriv
MeanValue
TangentCone
Complex
Polynomial
Basic
Arg
Asymptotics
Basic
CauchyIntegral
Circle
Conformal
Isometry
Liouville
ReImTopology
RealDeriv
Convex
Cone
Basic
Extension
SpecificFunctions
Basic
Basic
Between
Combination
Function
Gauge
Hull
Jensen
Mul
Normed
Segment
Slope
Star
Strict
StrictConvexSpace
Topology
Uniform
InnerProductSpace
Basic
GramSchmidtOrtho
Orientation
Orthogonal
PiL2
Projection
Symmetric
LocallyConvex
BalancedCoreHull
Basic
Bounded
Polar
WithSeminorms
Normed
Affine
AddTorsor
AddTorsorBases
Isometry
Field
Basic
InfiniteSum
Lemmas
UnitBall
Group
AddCircle
AddTorsor
BallSphere
Basic
Bounded
Completion
Constructions
Hom
InfiniteSum
Int
Lemmas
Pointwise
Quotient
Rat
Seminorm
Submodule
Uniform
Lp
PiLp
WithLp
Module
Basic
Completion
Dual
FiniteDimension
Ray
Span
Operator
Banach
BoundedLinearMaps
ContinuousLinearMap
LinearIsometry
Order
Basic
Lattice
Ring
Units
MulAction
NormedSpace
HahnBanach
Extension
SeparatingDual
Separation
Multilinear
Basic
Curry
OperatorNorm
Asymptotics
Basic
Bilinear
Completeness
Mul
NNNorm
NormedSpace
ConformalLinearMap
Extend
IndicatorFunction
Pointwise
RCLike
Real
RieszLemma
RCLike
Basic
Lemmas
SpecialFunctions
Complex
Arg
Log
Log
Base
Basic
Deriv
Pow
Asymptotics
Complex
Continuity
NNReal
Real
Trigonometric
Angle
Basic
Inverse
Exp
ExpDeriv
NonIntegrable
SpecificLimits
Basic
Normed
MeanInequalities
MeanInequalitiesPow
Oscillation
Seminorm
CategoryTheory
Adjunction
Basic
FullyFaithful
Bicategory
Functor
Lax
Oplax
Prelax
Pseudofunctor
Basic
Coherence
Free
LocallyDiscrete
Strict
Category
Basic
Cat
Init
Comma
Arrow
Basic
ConcreteCategory
Basic
Bundled
Functor
Basic
Category
Const
FullyFaithful
Trifunctor
Monoidal
Free
Basic
Coherence
Category
Functor
MorphismProperty
Basic
Pi
Basic
Products
Basic
Unitor
DiscreteCategory
EpiMono
EqToHom
Equivalence
EssentialImage
FullSubcategory
Groupoid
Iso
NatIso
NatTrans
Opposites
PathCategory
Quotient
Types
Whiskering
Combinatorics
Enumerative
Composition
Partition
Quiver
Basic
Path
Push
Symmetric
Control
Monad
Basic
Cont
Writer
Traversable
Basic
Lemmas
Applicative
Basic
Bifunctor
Combinators
EquivFunctor
Functor
Lawful
Random
ULift
ULiftable
Data
Array
Defs
Bool
Basic
Set
Complex
Abs
Basic
BigOperators
Cardinality
Exponential
FiniteDimensional
Module
Order
Countable
Basic
Defs
DFinsupp
Basic
Encodable
Lex
NeLocus
Order
ENNReal
Basic
Inv
Operations
Real
ENat
Basic
Lattice
Fin
Tuple
Basic
Basic
VecNotation
Finite
Basic
Card
Defs
Set
Finset
Attr
Basic
Card
Density
Fin
Fold
Image
Lattice
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
Piecewise
Powerset
Preimage
Prod
Sigma
Sort
Sum
Sym
Union
Update
Finsupp
Antidiagonal
Basic
Defs
Encodable
Fin
Fintype
Indicator
Lex
Multiset
Order
ToDFinsupp
Fintype
Basic
BigOperators
Card
CardEmbedding
Fin
Lattice
List
Option
Order
Parity
Perm
Pi
Powerset
Prod
Quotient
Sigma
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Order
Basic
Lemmas
Units
Bitwise
CharZero
ConditionallyCompleteOrder
Defs
GCD
Interval
LeastGreatest
Lemmas
Log
ModEq
Notation
Range
Sqrt
SuccPred
List
EditDistance
Bounds
Defs
Estimator
Basic
Chain
Count
Cycle
Dedup
Defs
Duplicate
FinRange
Forall2
GetD
Indexes
Infix
InsertNth
Join
Lattice
Lex
MinMax
Monad
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
ProdSigma
Range
Rotate
Sort
Sublists
Sym
TFAE
Zip
MLList
BestFirst
Matrix
Basic
Basis
Block
DMatrix
Invertible
Notation
RowCol
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
NatAntidiagonal
Nodup
OrderedMonoid
Pi
Powerset
Range
Sections
Sort
Sum
Sym
NNRat
Defs
Lemmas
Order
NNReal
Basic
Star
Nat
Cast
Order
Basic
Field
Ring
Basic
Commute
Defs
Field
NeZero
Prod
WithTop
Choose
Basic
Bounds
Sum
Factorial
Basic
Factorization
Basic
Defs
Induction
PrimePow
Fib
Basic
GCD
Basic
BigOperators
Order
Lemmas
Prime
Basic
Defs
Bits
Bitwise
Count
Defs
Digits
Factors
Find
Lattice
Log
MaxPowDiv
ModEq
Multiplicity
Notation
Pairing
PartENat
Periodic
PrimeFin
Set
Size
Sqrt
Squarefree
SuccPred
Totient
WithBot
Option
Basic
Defs
NAry
Ordering
Basic
PNat
Basic
Defs
Equiv
Prime
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
BigOperators
Finite
Interval
ListOfFn
SMul
Accumulate
Basic
BoolIndicator
Constructions
Countable
Defs
Finite
Function
Functor
Image
Lattice
List
MemPartition
NAry
Notation
Operations
Prod
Semiring
Sigma
Subset
Subsingleton
UnionLift
SetLike
Basic
Setoid
Basic
Sigma
Basic
Lex
String
Defs
Sum
Basic
Order
Sym
Sym2 (
file
)
Init
Order
Basic
Tree
Basic
Vector
Basic
Defs
W
Basic
Cardinal
ZMod
Algebra
Basic
Defs
IntUnitsPower
Module
Quotient
Units
Bracket
Opposite
Part
Quot
Rel
SProd
Sign
Subtype
ULift
Dynamics
Ergodic
MeasurePreserving
FixedPoints
Basic
Minimal
PeriodicPts
FieldTheory
Finite
Basic
GaloisField
Trace
IntermediateField
Algebraic
Basic
IsAlgClosed
AlgebraicClosure
Basic
Minpoly
Basic
Field
IsIntegrallyClosed
MinpolyDiv
RatFunc
AsPolynomial
Basic
Defs
SplittingField
Construction
IsSplittingField
Adjoin
Extension
Finiteness
Fixed
Galois
Normal
NormalClosure
Perfect
PolynomialGaloisGroup
PrimitiveElement
Separable
Tower
GroupTheory
Commutator
Basic
Congruence
Basic
Coset
Basic
Card
FreeGroup
Basic
GroupAction
DomAct
Basic
SubMulAction (
file
)
Pointwise
Basic
ConjAct
FixedPoints
FixingSubgroup
Hom
IterateAct
Pointwise
Quotient
Ring
MonoidLocalization
Basic
MonoidWithZero
Perm
Cycle
Basic
Factors
Type
Basic
Closure
Fin
Finite
List
Option
Sign
Support
ViaEmbedding
QuotientGroup
Basic
SpecificGroups
Cyclic
Subgroup
Center
Centralizer
Simple
Submonoid
Center
Centralizer
Subsemigroup
Center
Centralizer
Abelianization
Archimedean
Divisible
Exponent
Finiteness
FreeAbelianGroup
Index
OrderOfElement
PGroup
Solvable
Torsion
Init (
file
)
Algebra
Classes
Logic
Lean
Elab
Tactic
Basic
Term
Expr
Basic
ExtraRecognizers
ReplaceRec
Meta (
file
)
Basic
CongrTheorems
KAbstractPositions
Simp
PrettyPrinter
Delaborator
EnvExtension
GoalsLocation
Name
Thunk
LinearAlgebra
AffineSpace
AffineEquiv
AffineMap
AffineSubspace
Basic
Basis
Combination
FiniteDimensional
Independent
Midpoint
Pointwise
Restrict
Slope
Alternating
Basic
Basis
Basic
Bilinear
Cardinality
Defs
VectorSpace
BilinearForm
Basic
DualLattice
Hom
Properties
Dimension
Basic
Constructions
DivisionRing
Finite
Finrank
Free
FreeAndStrongRankCondition
LinearMap
RankNullity
StrongRankCondition
DirectSum
Finsupp
TensorProduct
FiniteDimensional (
file
)
Defs
FreeModule
Finite
Basic
Matrix
Basic
PID
StrongRankCondition
Matrix
Charpoly
Basic
Coeff
LinearMap
Minpoly
Determinant
Basic
GeneralLinearGroup
Basic
Defs
Adjugate
Basis
BilinearForm
Block
Diagonal
MvPolynomial
Nondegenerate
NonsingularInverse
Polynomial
Reindex
SesquilinearForm
SpecialLinearGroup
ToLin
ToLinearEquiv
Trace
Transvection
Multilinear
Basic
Basis
TensorProduct
Basic
Basis
Tower
BilinearMap
Contraction
DFinsupp
Determinant
Dual
Finsupp
FinsuppVectorSpace
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
LinearIndependent
LinearPMap
Orientation
Pi
Prod
Projection
Quotient
Ray
SModEq
SesquilinearForm
Span
StdBasis
Trace
UnitaryGroup
Vandermonde
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Basic
Defs
Embedding
Fin
Fintype
Functor
List
Nat
Option
PartialEquiv
Set
TransferInstance
Function
Basic
CompTypeclasses
Conjugate
Defs
Iterate
ULift
Nontrivial
Basic
Defs
Small
Basic
Defs
Set
Basic
Denumerable
ExistsUnique
IsEmpty
Lemmas
Nonempty
OpClass
Pairwise
Relation
Relator
Unique
MeasureTheory
Constructions
BorelSpace
Basic
Complex
ContinuousLinearMap
Metric
Metrizable
Order
Real
Prod
Basic
Integral
EventuallyMeasurable
Pi
Decomposition
Exhaustion
Function
LpSeminorm
Basic
ChebyshevMarkov
CompareExp
TriangleInequality
SpecialFunctions
Basic
StronglyMeasurable
Basic
Lemmas
AEEqFun
AEMeasurableSequence
EssSup
L1Space
LocallyIntegrable
LpOrder
LpSpace
SimpleFunc
SimpleFuncDense
SimpleFuncDenseLp
Group
Action
Arithmetic
Defs
LIntegral
MeasurableEquiv
Measure
Pointwise
Prod
Integral
Bochner
CircleIntegral
DivergenceTheorem
DominatedConvergence
FundThmCalculus
IntegrableOn
IntervalIntegral
Lebesgue
Marginal
MeanInequalities
SetIntegral
SetToL1
VitaliCaratheodory
MeasurableSpace
Basic
CountablyGenerated
Defs
Embedding
Instances
Measure
Haar
Basic
InnerProductSpace
OfBasis
Lebesgue
Basic
Complex
EqHaar
AEDisjoint
AEMeasurable
Content
Count
Dirac
Doubling
GiryMonad
MeasureSpace
MeasureSpaceDef
MutuallySingular
NullMeasurable
OpenPos
Regular
Restrict
Stieltjes
Trim
Typeclasses
WithDensity
Order
Lattice
OuterMeasure
AE
Basic
BorelCantelli
Caratheodory
Defs
Induced
OfFunction
Operations
PiSystem
NumberTheory
Cyclotomic
Basic
PrimitiveRoots
LegendreSymbol
QuadraticChar
Basic
GaussSum
AddCharacter
Basic
JacobiSymbol
QuadraticReciprocity
ZModChar
MulChar
Basic
NumberField
Basic
Padics
PadicVal
Basic
Defs
ArithmeticFunction
Divisors
GaussSum
Order
Bounds
Basic
OrderIso
CompactlyGenerated
Basic
Intervals
ConditionallyCompleteLattice
Basic
Finset
Group
Filter
AtTopBot (
file
)
Archimedean
BigOperators
Field
Group
ModEq
Monoid
Ring
Germ
Basic
Bases
Basic
Cofinite
CountableInter
CountableSeparatingOn
Curry
ENNReal
EventuallyConst
Extr
IndicatorFunction
Interval
Ker
Lift
NAry
Pi
Pointwise
Prod
SmallSets
Subsingleton
Ultrafilter
Fin
Basic
Tuple
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
RelIso
Basic
Set
SuccPred
Archimedean
Basic
CompleteLinearOrder
Limit
Relation
UpperLower
Basic
Antichain
Antisymmetrization
Atoms
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
Compare
CompleteBooleanAlgebra
CompleteLattice
CompleteLatticeIntervals
Copy
Cover
Defs
Directed
Disjoint
Disjointed
Estimator
FixedPoints
GaloisConnection
InitialSeg
Iterate
JordanHolder
Lattice
LatticeIntervals
LiminfLimsup
Max
MinMax
Minimal
ModularLattice
Nat
Notation
OmegaCompletePartialOrder
OrderIsoNat
Part
PartialSups
PiLex
PropInstances
RelClasses
RelSeries
ScottContinuity
SetNotation
SupClosed
SupIndep
SymmDiff
Synonym
TypeTags
ULift
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
RingTheory
Adjoin
Basic
FG
Field
PowerBasis
Tower
Congruence
Basic
Coprime
Basic
Ideal
Lemmas
DedekindDomain
AdicValuation
Basic
Ideal
IntegralClosure
FractionalIdeal
Basic
Operations
Ideal
Basic
Colon
IsPrimary
Maps
Operations
Over
Prod
Quotient
QuotientOperations
Int
Basic
IntegralClosure
Algebra
Basic
Defs
IsIntegral
Basic
Defs
IsIntegralClosure
Basic
Defs
IntegrallyClosed
LocalRing
MaximalIdeal
Basic
Defs
ResidueField
Basic
Defs
RingHom
Basic
Defs
Basic
Defs
Localization
AsSubring
AtPrime
Basic
FractionRing
Ideal
Integer
Integral
LocalizationLocalization
Module
NumDen
Submodule
MvPolynomial
Symmetric
Defs
Tower
Nilpotent
Basic
Defs
Lemmas
NonUnitalSubring
Basic
NonUnitalSubsemiring
Basic
Norm
Basic
Defs
OreLocalization
Basic
OreSet
Ring
Polynomial
Cyclotomic
Basic
Eval
Expand
Roots
Eisenstein
Basic
Basic
Content
GaussLemma
IntegralNormalization
Nilpotent
Pochhammer
Quotient
RationalRoot
ScaleRoots
Tower
Vieta
RootsOfUnity
Basic
Complex
Minpoly
TensorProduct
Basic
Trace
Basic
Defs
Valuation
Basic
ExtendToLocalization
Integers
ValuationRing
ValuationSubring
AdjoinRoot
AlgebraTower
Algebraic
Bezout
ChainOfDivisors
EisensteinCriterion
EuclideanDomain
FinitePresentation
FiniteType
Finiteness
FreeCommRing
FreeRing
IntegralDomain
JacobsonIdeal
MatrixAlgebra
MaximalSpectrum
Multiplicity
Noetherian
OrzechProperty
PolynomialAlgebra
PowerBasis
Prime
PrimeSpectrum
PrincipalIdealDomain
QuotientNoetherian
SimpleModule
UniqueFactorizationDomain
ZMod
SetTheory
Cardinal
Basic
Cofinality
Continuum
ENat
Finite
Finsupp
Ordinal
PartENat
SchroederBernstein
Subfield
ToNat
Ordinal
Arithmetic
Basic
Exponential
FixedPoint
Principal
Std
Data
HashMap
Tactic (
file
)
ArithMult (
file
)
Init
Attr
Core
Register
Bound (
file
)
Attribute
Init
CC (
file
)
Addition
Datatypes
Lemmas
CancelDenoms (
file
)
Core
CategoryTheory
Bicategory
Basic
Datatypes
Normalize
PureCoherence
Coherence (
file
)
Basic
Datatypes
Normalize
PureCoherence
Monoidal
Basic
Datatypes
Normalize
PureCoherence
BicategoricalComp
BicategoryCoherence
Elementwise
MonoidalComp
Reassoc
Slice
ToApp
Continuity (
file
)
Init
Explode (
file
)
Datatypes
Pretty
FunProp (
file
)
Attr
ContDiff
Core
Decl
Differentiable
Elab
FunctionData
Mor
RefinedDiscrTree
StateList
Theorems
ToBatteries
Types
GCongr (
file
)
Core
CoreAttrs
ForwardAttr
Linarith (
file
)
Oracle
SimplexAlgorithm (
file
)
Datatypes
Gauss
PositiveVector
SimplexAlgorithm
FourierMotzkin
Datatypes
Frontend
Lemmas
Parsing
Preprocessing
Verification
LinearCombination (
file
)
Lemmas
Linter (
file
)
AdmitLinter
DocPrime
FlexibleLinter
GlobalAttributeIn
HashCommandLinter
HaveLetLinter
Lint
MinImports
OldObtain
RefineLinter
Style
TextBased
UnusedTactic
Measurability (
file
)
Init
Monotonicity (
file
)
Attr
Basic
Lemmas
Nontriviality (
file
)
Core
NormNum (
file
)
Basic
BigOperators
Core
DivMod
Eq
GCD
Ineq
Inv
IsCoprime
LegendreSymbol
NatFib
NatSqrt
OfScientific
Pow
Prime
Result
Positivity (
file
)
Basic
Core
Finset
ReduceModChar (
file
)
Ext
Relation
Rfl
Symm
Trans
Ring (
file
)
Basic
PNat
RingNF
Sat
FromLRAT
Simps
Basic
NotationClass
ToAdditive (
file
)
Frontend
Widget
Calc
CommDiag
CongrM
Conv
GCongr
InteractiveUnfold
SelectInsertParamsClass
SelectPanelUtils
StringDiagram
Abel
AdaptationNote
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Basic
ByContra
Cases
CasesM
Change
Check
Choose
Clean
ClearExcept
ClearExclamation
Clear_
Coe
Common
ComputeDegree
CongrExclamation
CongrM
Constructor
ContinuousFunctionalCalculus
Contrapose
Conv
Convert
Core
DefEqTransformations
DeprecateMe
DeriveFintype
DeriveToExpr
DeriveTraversable
Eqns
Eval
ExistsI
ExtendDoc
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
Generalize
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
Have
HaveI
HelpCmd
HigherOrder
Hint
ITauto
InferParam
Inhabit
IntervalCases
IrreducibleDef
Lemma
Lift
LiftLets
LinearCombination'
MinImports
MkIffOfInductiveProp
ModCases
Module
MoveAdd
NoncommRing
NthRewrite
Observe
PPWithUniv
Peel
Polyrith
ProdAssoc
ProjectionNotation
Propose
ProxyType
PushNeg
Qify
RSuffices
Recall
Recover
Rename
RenameBVar
Replace
RewriteSearch
Rify
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SlimCheck
SplitIfs
Spread
StacksAttribute
Subsingleton
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TermCongr
ToExpr
ToLevel
Trace
TryThis
TypeCheck
TypeStar
UnsetOption
Use
Variable
WLOG
Zify
Testing
SlimCheck
Gen
Sampleable
Testable
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
WeakBilin
Nonarchimedean
Bases
Basic
Order
Archimedean
Compact
Field
Group
LiminfLimsup
Rolle
Ring
Basic
Ideal
Valued
ValuationTopology
ValuedField
Affine
Algebra
ConstMulAction
Constructions
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Monoid
MulAction
OpenSubgroup
Polynomial
Star
UniformConvergence
UniformField
UniformFilterBasis
UniformGroup
UniformMulAction
UniformRing
WithZeroTopology
Baire
CompleteMetrizable
Lemmas
Bornology
Absorbs
Basic
BoundedOperation
Constructions
Hom
Compactness
Compact
Lindelof
LocallyCompact
SigmaCompact
Connected
Basic
Clopen
LocallyConnected
PathConnected
TotallyDisconnected
ContinuousFunction
Algebra
Basic
Bounded
CocompactMap
Compact
ContinuousMapZero
Ordered
Defs
Basic
Filter
Induced
Sequences
EMetricSpace
Basic
Defs
Diam
Lipschitz
Pi
FiberBundle
IsHomeomorphicTrivialBundle
Instances
AddCircle
Discrete
ENNReal
EReal
Int
Matrix
NNReal
Nat
Rat
Real
RealVectorSpace
Sign
Maps
Proper
Basic
Basic
MetricSpace
Pseudo
Basic
Constructions
Defs
Lemmas
Pi
Real
Algebra
Antilipschitz
Basic
Bounded
Cauchy
Completion
Defs
Dilation
DilationEquiv
Equicontinuity
HausdorffDistance
IsometricSMul
Isometry
Lipschitz
ProperSpace
ThickenedIndicator
Thickening
Metrizable
Basic
Uniformity
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
DenseEmbedding
DiscreteSubset
ExtendFrom
Filter
GDelta
Homeomorph
IndicatorConstPointwise
Inseparable
Irreducible
IsLocalHomeomorph
LocallyFinite
NhdsSet
NoetherianSpace
PartialHomeomorph
QuasiSeparated
RestrictGen
Semicontinuous
SeparatedMap
Separation
Sequences
Support
UnitInterval
Util
AddRelatedDecl
AssertExists
AssertExistsExt
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
MemoFix
Notation3
Qq
SynthesizeUsing
Tactic
WhatsNew
WithWeakNamespace
ProofWidgets
Component
Panel
Basic
Basic
HtmlDisplay
MakeEditLink
OfRpcMethod
PenroseDiagram
Data
Html
Presentation
Expr
Cancellable
Compat
Util
Qq (
file
)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
SortLocalDecls
Typ
Std (
file
)
Data (
file
)
DHashMap (
file
)
Internal
AssocList
Basic
Lemmas
List
Associative
Defs
HashesTo
Pairwise
Sublist
Defs
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
Lemmas
Raw
RawDef
RawLemmas
HashMap (
file
)
AdditionalOperations
Basic
Lemmas
Raw
RawLemmas
HashSet (
file
)
Basic
Lemmas
Raw
RawLemmas
Internal (
file
)
Parsec (
file
)
Basic
ByteArray
String
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
Tactic (
file
)
BVDecide (
file
)
Bitblast (
file
)
BVExpr (
file
)
Circuit (
file
)
Impl (
file
)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Ult
ZeroExtend
Carry
Const
Expr
Pred
Var
Lemmas (
file
)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Ult
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
equational_theories (
file
)
Generated (
file
)
SimpleRewrites (
file
)
theorems
Rewrite_uw
Rewrite_uw_vu
Rewrite_uw_vu_wx
Rewrite_uw_vu_wy
Rewrite_uw_vu_wz
Rewrite_uw_vu_wz_yx_zy
Rewrite_uw_vu_wz_zx
Rewrite_uw_vu_wz_zy
Rewrite_uw_wx
Rewrite_uw_wy
Rewrite_uw_wz
Rewrite_uw_wz_yx_zy
Rewrite_uw_wz_zx
Rewrite_uw_wz_zy
Rewrite_ux
Rewrite_ux_vu
Rewrite_uy
Rewrite_uy_vu
Rewrite_uz
Rewrite_uz_vu
Rewrite_vu
Rewrite_vw
Rewrite_vx
Rewrite_vy
Rewrite_vz
Rewrite_wx
Rewrite_wy
Rewrite_wz
Rewrite_wz_yx_zy
Rewrite_wz_zx
Rewrite_wz_zy
Rewrite_yx
Rewrite_yx_zy
Rewrite_zx
Rewrite_zy
TrivialBruteforce (
file
)
theorems
Apply
Apply2
RewriteGoal
RewriteHypothesis
RewriteHypothesisAndGoal
Constant
Singleton
AllEquations
Conjecture
Equations
EquationsCommand
InfModel
Magma
ParseImplications
Subgraph
find
index
404
foundational_types
index
navbar
references
search
equational_theories (
file
)
ForMathlib
Algebra
Group
Nat
Generated (
file
)
All4x4Tables (
file
)
Refutation0
Refutation1
Refutation10
Refutation100
Refutation101
Refutation102
Refutation103
Refutation104
Refutation105
Refutation106
Refutation107
Refutation108
Refutation109
Refutation11
Refutation110
Refutation111
Refutation112
Refutation113
Refutation114
Refutation115
Refutation116
Refutation117
Refutation118
Refutation119
Refutation12
Refutation120
Refutation121
Refutation122
Refutation123
Refutation124
Refutation125
Refutation126
Refutation127
Refutation128
Refutation129
Refutation13
Refutation130
Refutation131
Refutation132
Refutation133
Refutation134
Refutation135
Refutation136
Refutation137
Refutation138
Refutation139
Refutation14
Refutation140
Refutation141
Refutation142
Refutation143
Refutation144
Refutation145
Refutation146
Refutation147
Refutation148
Refutation149
Refutation15
Refutation150
Refutation151
Refutation152
Refutation153
Refutation154
Refutation155
Refutation156
Refutation157
Refutation158
Refutation159
Refutation16
Refutation160
Refutation161
Refutation162
Refutation163
Refutation164
Refutation165
Refutation166
Refutation167
Refutation168
Refutation169
Refutation17
Refutation170
Refutation171
Refutation172
Refutation173
Refutation174
Refutation175
Refutation176
Refutation177
Refutation178
Refutation179
Refutation18
Refutation180
Refutation181
Refutation182
Refutation183
Refutation184
Refutation185
Refutation186
Refutation187
Refutation188
Refutation189
Refutation19
Refutation190
Refutation191
Refutation192
Refutation193
Refutation194
Refutation195
Refutation196
Refutation197
Refutation198
Refutation199
Refutation2
Refutation20
Refutation200
Refutation201
Refutation202
Refutation203
Refutation204
Refutation205
Refutation206
Refutation207
Refutation208
Refutation209
Refutation21
Refutation210
Refutation211
Refutation212
Refutation213
Refutation214
Refutation215
Refutation216
Refutation217
Refutation218
Refutation219
Refutation22
Refutation220
Refutation221
Refutation222
Refutation223
Refutation224
Refutation225
Refutation226
Refutation227
Refutation228
Refutation229
Refutation23
Refutation230
Refutation231
Refutation232
Refutation233
Refutation234
Refutation235
Refutation236
Refutation237
Refutation238
Refutation239
Refutation24
Refutation240
Refutation241
Refutation242
Refutation243
Refutation244
Refutation245
Refutation246
Refutation247
Refutation248
Refutation249
Refutation25
Refutation250
Refutation251
Refutation252
Refutation253
Refutation254
Refutation255
Refutation256
Refutation257
Refutation258
Refutation259
Refutation26
Refutation260
Refutation261
Refutation262
Refutation263
Refutation264
Refutation265
Refutation266
Refutation267
Refutation268
Refutation269
Refutation27
Refutation270
Refutation271
Refutation272
Refutation273
Refutation274
Refutation275
Refutation276
Refutation277
Refutation278
Refutation279
Refutation28
Refutation280
Refutation281
Refutation282
Refutation283
Refutation284
Refutation285
Refutation286
Refutation287
Refutation288
Refutation289
Refutation29
Refutation290
Refutation291
Refutation292
Refutation293
Refutation294
Refutation295
Refutation296
Refutation297
Refutation298
Refutation299
Refutation3
Refutation30
Refutation300
Refutation301
Refutation302
Refutation303
Refutation304
Refutation305
Refutation306
Refutation307
Refutation308
Refutation309
Refutation31
Refutation310
Refutation311
Refutation312
Refutation313
Refutation314
Refutation315
Refutation316
Refutation317
Refutation318
Refutation319
Refutation32
Refutation320
Refutation321
Refutation322
Refutation323
Refutation324
Refutation325
Refutation326
Refutation327
Refutation328
Refutation329
Refutation33
Refutation330
Refutation331
Refutation332
Refutation333
Refutation334
Refutation335
Refutation336
Refutation337
Refutation338
Refutation339
Refutation34
Refutation340
Refutation341
Refutation342
Refutation343
Refutation344
Refutation345
Refutation346
Refutation347
Refutation348
Refutation349
Refutation35
Refutation350
Refutation351
Refutation352
Refutation353
Refutation354
Refutation355
Refutation356
Refutation357
Refutation358
Refutation359
Refutation36
Refutation360
Refutation361
Refutation362
Refutation363
Refutation364
Refutation365
Refutation366
Refutation367
Refutation368
Refutation369
Refutation37
Refutation370
Refutation371
Refutation372
Refutation373
Refutation374
Refutation375
Refutation376
Refutation377
Refutation378
Refutation379
Refutation38
Refutation380
Refutation381
Refutation382
Refutation383
Refutation384
Refutation385
Refutation386
Refutation387
Refutation388
Refutation389
Refutation39
Refutation390
Refutation391
Refutation392
Refutation393
Refutation394
Refutation395
Refutation396
Refutation397
Refutation398
Refutation399
Refutation4
Refutation40
Refutation400
Refutation401
Refutation402
Refutation403
Refutation404
Refutation405
Refutation406
Refutation407
Refutation408
Refutation409
Refutation41
Refutation410
Refutation411
Refutation412
Refutation413
Refutation414
Refutation415
Refutation416
Refutation417
Refutation418
Refutation419
Refutation42
Refutation420
Refutation421
Refutation422
Refutation423
Refutation424
Refutation425
Refutation426
Refutation427
Refutation428
Refutation429
Refutation43
Refutation430
Refutation431
Refutation432
Refutation433
Refutation434
Refutation435
Refutation436
Refutation437
Refutation438
Refutation439
Refutation44
Refutation440
Refutation441
Refutation442
Refutation443
Refutation444
Refutation445
Refutation446
Refutation447
Refutation448
Refutation449
Refutation45
Refutation450
Refutation451
Refutation452
Refutation453
Refutation454
Refutation455
Refutation456
Refutation457
Refutation458
Refutation459
Refutation46
Refutation460
Refutation461
Refutation462
Refutation463
Refutation464
Refutation465
Refutation466
Refutation467
Refutation468
Refutation469
Refutation47
Refutation470
Refutation471
Refutation472
Refutation473
Refutation474
Refutation475
Refutation476
Refutation477
Refutation478
Refutation479
Refutation48
Refutation480
Refutation481
Refutation482
Refutation483
Refutation484
Refutation485
Refutation486
Refutation487
Refutation488
Refutation489
Refutation49
Refutation490
Refutation491
Refutation492
Refutation493
Refutation494
Refutation495
Refutation496
Refutation497
Refutation498
Refutation499
Refutation5
Refutation50
Refutation500
Refutation501
Refutation502
Refutation503
Refutation504
Refutation505
Refutation506
Refutation507
Refutation508
Refutation509
Refutation51
Refutation510
Refutation511
Refutation512
Refutation513
Refutation514
Refutation515
Refutation516
Refutation517
Refutation518
Refutation519
Refutation52
Refutation520
Refutation521
Refutation522
Refutation523
Refutation524
Refutation525
Refutation526
Refutation527
Refutation528
Refutation529
Refutation53
Refutation530
Refutation531
Refutation532
Refutation533
Refutation534
Refutation535
Refutation536
Refutation537
Refutation538
Refutation539
Refutation54
Refutation540
Refutation541
Refutation542
Refutation543
Refutation544
Refutation545
Refutation546
Refutation547
Refutation548
Refutation549
Refutation55
Refutation550
Refutation551
Refutation552
Refutation553
Refutation554
Refutation555
Refutation556
Refutation557
Refutation558
Refutation559
Refutation56
Refutation560
Refutation561
Refutation562
Refutation563
Refutation564
Refutation565
Refutation566
Refutation567
Refutation568
Refutation569
Refutation57
Refutation570
Refutation571
Refutation572
Refutation573
Refutation574
Refutation575
Refutation576
Refutation577
Refutation578
Refutation579
Refutation58
Refutation580
Refutation581
Refutation582
Refutation583
Refutation584
Refutation585
Refutation586
Refutation587
Refutation588
Refutation589
Refutation59
Refutation590
Refutation591
Refutation592
Refutation593
Refutation594
Refutation595
Refutation596
Refutation597
Refutation598
Refutation599
Refutation6
Refutation60
Refutation600
Refutation601
Refutation602
Refutation603
Refutation604
Refutation605
Refutation606
Refutation607
Refutation608
Refutation609
Refutation61
Refutation610
Refutation611
Refutation612
Refutation613
Refutation614
Refutation615
Refutation616
Refutation617
Refutation618
Refutation619
Refutation62
Refutation620
Refutation621
Refutation622
Refutation623
Refutation624
Refutation625
Refutation626
Refutation627
Refutation628
Refutation629
Refutation63
Refutation630
Refutation631
Refutation632
Refutation633
Refutation634
Refutation635
Refutation636
Refutation637
Refutation638
Refutation639
Refutation64
Refutation640
Refutation641
Refutation642
Refutation643
Refutation644
Refutation645
Refutation646
Refutation647
Refutation648
Refutation649
Refutation65
Refutation650
Refutation651
Refutation652
Refutation653
Refutation654
Refutation655
Refutation656
Refutation657
Refutation658
Refutation659
Refutation66
Refutation660
Refutation661
Refutation662
Refutation663
Refutation664
Refutation665
Refutation666
Refutation667
Refutation668
Refutation669
Refutation67
Refutation670
Refutation671
Refutation672
Refutation673
Refutation674
Refutation675
Refutation676
Refutation677
Refutation678
Refutation679
Refutation68
Refutation680
Refutation681
Refutation682
Refutation683
Refutation684
Refutation685
Refutation686
Refutation687
Refutation688
Refutation689
Refutation69
Refutation690
Refutation691
Refutation692
Refutation693
Refutation694
Refutation695
Refutation696
Refutation697
Refutation698
Refutation699
Refutation7
Refutation70
Refutation700
Refutation701
Refutation702
Refutation703
Refutation704
Refutation705
Refutation706
Refutation707
Refutation708
Refutation709
Refutation71
Refutation710
Refutation711
Refutation712
Refutation713
Refutation714
Refutation715
Refutation716
Refutation717
Refutation718
Refutation719
Refutation72
Refutation720
Refutation721
Refutation722
Refutation723
Refutation724
Refutation725
Refutation726
Refutation727
Refutation728
Refutation729
Refutation73
Refutation730
Refutation731
Refutation732
Refutation733
Refutation734
Refutation735
Refutation736
Refutation737
Refutation738
Refutation739
Refutation74
Refutation740
Refutation741
Refutation742
Refutation743
Refutation744
Refutation75
Refutation76
Refutation77
Refutation78
Refutation79
Refutation8
Refutation80
Refutation81
Refutation82
Refutation83
Refutation84
Refutation85
Refutation86
Refutation87
Refutation88
Refutation89
Refutation9
Refutation90
Refutation91
Refutation92
Refutation93
Refutation94
Refutation95
Refutation96
Refutation97
Refutation98
Refutation99
Confluence (
file
)
ManuallySampled
EquationSearch (
file
)
theorems
Combined
Run1
Run2
Run3
Run4
Run5
Run6
Run7
FinSearch (
file
)
theorems
Refutation0
Refutation1
Refutation2
Refutation3
Refutation4
Refutation5
FinitePoly (
file
)
Refutation108
Refutation112
Refutation114
Refutation116
Refutation120
Refutation126
Refutation128
Refutation132
Refutation138
Refutation14
Refutation144
Refutation146
Refutation150
Refutation152
Refutation154
Refutation172
Refutation174
Refutation176
Refutation178
Refutation18
Refutation184
Refutation190
Refutation194
Refutation196
Refutation198
Refutation20
Refutation200
Refutation206
Refutation208
Refutation212
Refutation214
Refutation216
Refutation218
Refutation220
Refutation226
Refutation232
Refutation234
Refutation236
Refutation238
Refutation24
Refutation246
Refutation250
Refutation26
Refutation262
Refutation264
Refutation268
Refutation270
Refutation272
Refutation280
Refutation284
Refutation286
Refutation290
Refutation302
Refutation312
Refutation314
Refutation316
Refutation318
Refutation32
Refutation320
Refutation326
Refutation328
Refutation330
Refutation34
Refutation340
Refutation342
Refutation344
Refutation346
Refutation352
Refutation356
Refutation364
Refutation366
Refutation370
Refutation374
Refutation380
Refutation386
Refutation388
Refutation390
Refutation394
Refutation40
Refutation400
Refutation402
Refutation404
Refutation406
Refutation408
Refutation410
Refutation418
Refutation420
Refutation422
Refutation424
Refutation426
Refutation432
Refutation444
Refutation454
Refutation46
Refutation470
Refutation472
Refutation474
Refutation476
Refutation482
Refutation488
Refutation492
Refutation50
Refutation502
Refutation532
Refutation550
Refutation56
Refutation568
Refutation6
Refutation60
Refutation620
Refutation622
Refutation636
Refutation656
Refutation66
Refutation664
Refutation672
Refutation674
Refutation676
Refutation68
Refutation682
Refutation690
Refutation72
Refutation74
Refutation78
Refutation8
Refutation82
Refutation84
Refutation88
Refutation90
Refutation92
Refutation94
Refutation96
MagmaEgg
small (
file
)
_000
_001
_002
_003
_004
_005
_006
_007
_008
_009
_010
_011
_012
_013
_014
_015
_016
_017
_018
SimpleRewrites (
file
)
theorems
Rewrite_uw
Rewrite_uw_vu
Rewrite_uw_vu_wx
Rewrite_uw_vu_wy
Rewrite_uw_vu_wz
Rewrite_uw_vu_wz_yx_zy
Rewrite_uw_vu_wz_zx
Rewrite_uw_vu_wz_zy
Rewrite_uw_wx
Rewrite_uw_wy
Rewrite_uw_wz
Rewrite_uw_wz_yx_zy
Rewrite_uw_wz_zx
Rewrite_uw_wz_zy
Rewrite_ux
Rewrite_ux_vu
Rewrite_uy
Rewrite_uy_vu
Rewrite_uz
Rewrite_uz_vu
Rewrite_vu
Rewrite_vw
Rewrite_vx
Rewrite_vy
Rewrite_vz
Rewrite_wx
Rewrite_wy
Rewrite_wz
Rewrite_wz_yx_zy
Rewrite_wz_zx
Rewrite_wz_zy
Rewrite_yx
Rewrite_yx_zy
Rewrite_zx
Rewrite_zy
TrivialBruteforce (
file
)
theorems
Apply
Apply2
NthRewrites
RewriteCombinations
RewriteGoal
RewriteHypothesis
RewriteHypothesisAndGoal
Vampire (
file
)
Vampire_conjecture_15458
Vampire_conjecture_17205
Vampire_conjecture_1804
Vampire_conjecture_24431
Vampire_conjecture_27361
Vampire_conjecture_28479
Vampire_conjecture_31303
Vampire_conjecture_32785
Vampire_conjecture_35471
Vampire_conjecture_38574
Vampire_conjecture_41209
Vampire_conjecture_41555
Vampire_conjecture_41820
Vampire_conjecture_47854
Vampire_conjecture_50251
Vampire_conjecture_50368
Vampire_conjecture_51871
Vampire_conjecture_55174
Vampire_conjecture_55570
Vampire_conjecture_58537
Vampire_conjecture_62848
Vampire_conjecture_75635
Vampire_conjecture_77692
Vampire_conjecture_79507
Vampire_conjecture_80705
Vampire_conjecture_88223
Vampire_conjecture_88701
Vampire_conjecture_90304
Vampire_conjecture_90525
VampireProven (
file
)
Conjectures
Disproofs1
Disproofs2
Disproofs3
Disproofs4
Disproofs5
Disproofs6
Disproofs7
Disproofs8
Proofs1
Proofs10
Proofs11
Proofs12
Proofs13
Proofs2
Proofs3
Proofs4
Proofs5
Proofs6
Proofs7
Proofs8
Proofs9
Constant
Equation1
Singleton
AllEquations
CentralGroupoids
Closure
Compactness
Completeness
Confluence
Conjecture
Counting
DecideBang
EquationLawConversion
EquationalResult
Equations
EquationsCommand
FactsSyntax
FactsSyntaxExamples
FreeComm
FreeMagma
FreeMagmaImplications
FreeSemigroup
Homomorphisms
InfModel
InfiniteModels
LinearOps
Magma
MagmaLaw
MagmaOp
MemoFinOp
OrderMetatheorem
ParseImplications
Preorder
SmallMagmas
StringMagmas
Subgraph
Superposition
Z3Counterexamples
references (
file
)
Color scheme
dark
system
light