General documentation

index

foundational types

tactics

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

UpdateGoal

LevelIndex

PremiseIndex

RuleInfo

SlotIndex

Substitution

Frontend (file)

Extension (file)

Init

Attribute

Basic

Command

RuleExpr

Saturate

Tactic

Index (file)

Basic

DiscrTreeConfig

Forward

RulePattern

Options

Internal

Public

Rule (file)

Basic

Forward

Name

RulePattern (file)

Cache

RuleSet (file)

Filter

Member

Name

RuleTac (file)

Forward (file)

Basic

Apply

Basic

Cases

Descr

ElabRuleTerm

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

File

Report

Tree

Data (file)

ForwardRuleMatches

AddRapp

Check

ExtractProof

ExtractScript

Free

RunMetaM

State

Stats

Tracing

Traversal

TreeM

UnsafeQueue

Util

Tactic (file)

Ext

Unfold

Basic

EqualUpToIds

OrderedHashSet

Unfold

UnionFind

UnorderedArraySet

BaseM

Check

Constants

EMap

ElabM

Exception

Main

Nanos

Percent

Saturate

Tracing

Archive

Sensitivity

Batteries

Classes

Order

RatCast

CodeAction (file)

Attr

Basic

Deprecated

Match

Misc

Control

ForInStep

Basic

Lemmas

Nondet

Basic

AlternativeMonad

LawfulMonadState

Lemmas

OptionT

Data

Array

Basic

Merge

BinomialHeap

Basic

Fin

Basic

Lemmas

List

Basic

Count

Lemmas

Pairwise

Perm

MLList

Basic

Nat

Bitwise (file)

Lemmas

Basic

Lemmas

UInt

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

Case

Congr

Exact

GeneralizeProofs

HelpCmd

Init

OpenPrivate

PermuteGoals

SeqFocus

Trans

Unreachable

Util

Cache

ExtendedBinder

LibraryNote

ProofWanted

Logic

ImportGraph

Graph

TransitiveClosure

Imports

ImportGraph

Redundant

RequiredModules

Lean

Environment

Tools (file)

FindHome

ImportDiff

MinImports

RedundantImports

Init (file)

Control (file)

Lawful (file)

MonadAttach (file)

Instances

Lemmas

MonadLift (file)

Basic

Instances

Lemmas

Basic

Instances

Lemmas

Basic

Do

EState

Except

ExceptCps

Id

MonadAttach

Option

Reader

State

StateCps

StateRef

Data (file)

Array (file)

Lex (file)

Basic

Lemmas

QSort (file)

Basic

Sort (file)

Basic

Lemmas

Subarray (file)

Split

Attach

Basic

BasicAux

BinSearch

Bootstrap

Count

DecidableEq

Erase

Extract

FinRange

Find

GetLit

InsertIdx

InsertionSort

Int

Lemmas

MapIdx

Mem

MinMax

Monadic

Nat

OfFn

Perm

Range

Set

TakeDrop

Zip

BitVec (file)

Basic

BasicAux

Bitblast

Bootstrap

Decidable

Folds

Lemmas

ByteArray (file)

Basic

Bootstrap

Extra

Lemmas

Char (file)

Basic

Lemmas

Order

Ordinal

Dyadic (file)

Basic

Instances

Inv

Round

Fin (file)

Basic

Bitwise

Fold

Iterate

Lemmas

Log2

OverflowAware

FloatArray (file)

Basic

Format (file)

Basic

Instances

Macro

Syntax

Int (file)

Bitwise (file)

Basic

Lemmas

DivMod (file)

Basic

Bootstrap

Lemmas

Pow

Basic

Compare

Cooper

Gcd

Lemmas

LemmasAux

Linear

OfNat

Order

Pow

Repr

ToString

Iterators (file)

Combinators (file)

Monadic (file)

Append

Attach

FilterMap

FlatMap

Take

ULift

Append

Attach

FilterMap

FlatMap

Take

ULift

Consumers (file)

Monadic (file)

Access

Collect

Loop

Partial

Total

Access

Collect

Loop

Partial

Stream

Total

Internal (file)

LawfulMonadLiftFunction

Lemmas (file)

Combinators (file)

Monadic (file)

Append

Attach

FilterMap

FlatMap

Take

ULift

Append

Attach

FilterMap

FlatMap

Take

ULift

Consumers (file)

Monadic (file)

Collect

Loop

Access

Collect

Loop

Monadic

Basic

Producers (file)

Monadic (file)

List

List

Basic

Producers (file)

Monadic (file)

List

List

Basic

PostconditionMonad

ToIterator

List (file)

Int (file)

Prod

Sum

Nat (file)

BEq

Basic

Count

Erase

Find

InsertIdx

Modify

Pairwise

Perm

Prod

Range

Sublist

Sum

TakeDrop

Scan (file)

Basic

Lemmas

Sort (file)

Basic

Impl

Lemmas

SplitOn (file)

Basic

Lemmas

Attach

Basic

BasicAux

Control

ControlImpl

Count

Erase

FinRange

Find

Impl

Lemmas

Lex

MapIdx

MinMax

MinMaxIdx

MinMaxOn

Monadic

Notation

OfFn

Pairwise

Perm

Range

Sublist

TakeDrop

ToArray

ToArrayImpl

Zip

Nat (file)

Bitwise (file)

Basic

Lemmas

Div (file)

Basic

Lemmas

Power2 (file)

Basic

Lemmas

Sqrt (file)

Basic

Lemmas

Basic

Compare

Control

Coprime

Dvd

Fold

Gcd

Lcm

Lemmas

Linear

Log2

MinMax

Mod

Order

SOM

Simproc

ToString

Option (file)

Array

Attach

Basic

BasicAux

Coe

Function

Instances

Lemmas

List

Monadic

Ord (file)

Array

Basic

BitVec

SInt

String

UInt

Vector

Order (file)

Classes

ClassesExtra

Factories

FactoriesExtra

Lemmas

LemmasExtra

MinMaxOn

Opposite

Ord

PackageFactories

Range (file)

Polymorphic (file)

Internal

SignedBitVec

Basic

BitVec

Char

Fin

GetElemTactic

Instances

Int

IntLemmas

Iterators

Lemmas

Map

Nat

NatLemmas

PRange

RangeIterator

SInt

Stream

UInt

UpwardEnumerable

Basic

Lemmas

Rat (file)

Basic

Lemmas

SInt (file)

Basic

Bitwise

Float

Float32

Lemmas

Slice (file)

Array (file)

Basic

Iterator

Lemmas

List (file)

Basic

Iterator

Lemmas

Basic

InternalLemmas

Lemmas

Notation

Operations

String (file)

Iter (file)

Basic

Intercalate

Lemmas (file)

Pattern (file)

Find (file)

Basic

Char

Pred

String

Split (file)

Basic

Char

Pred

String (file)

Basic

ForwardPattern

ForwardSearcher

TakeDrop (file)

Basic

Char

Pred

String

Basic

Char

Memcmp

Pred

Basic

FindPos

Hashable

Intercalate

IsEmpty

Iter

Iterate

Length

Modify

Order

Search

Slice

Splits

StringOrder

TakeDrop

Pattern (file)

Basic

Char

Pred

String

Basic

Bootstrap

Decode

Defs

Extra

FindPos

Hashable

Iterate

Iterator

Legacy

Length

Modify

OrderInstances

PosRaw

Search

Slice

Stream

Subslice

Substring

TakeDrop

Termination

ToSlice

Subtype (file)

Basic

Order

OrderExtra

Sum (file)

Basic

Lemmas

ToString (file)

Basic

Extra

Macro

Name

UInt (file)

Basic

BasicAux

Bitwise

Lemmas

Log2

Vector (file)

Algebra

Attach

Basic

Count

DecidableEq

Erase

Extract

FinRange

Find

InsertIdx

Int

Lemmas

Lex

MapIdx

Monadic

Nat

OfFn

Perm

Range

Stream

Zip

AC

BEq

Bool

Cast

Float

Float32

Function

Hashable

LawfulHashable

NeZero

OfScientific

PLift

Prod

Queue

RArray

Random

Repr

Stream

ULift

Zero

Grind (file)

Module (file)

Basic

Envelope

NatModuleNorm

OfNatModule

Ordered (file)

Field

Int

Linarith

Module

Order

Rat

Ring

Ring (file)

Basic

CommSemiringAdapter

CommSolver

Envelope

Field

OfScientific

ToInt

AC

Annotated

Attr

Cases

Config

Ext

FieldNormNum

Injective

Interactive

Lemmas

Lint

Norm

Offset

Order

PP

Propagator

Tactics

ToInt

ToIntLemmas

Util

GrindInstances (file)

Ring (file)

BitVec

Fin

Int

Nat

Rat

SInt

UInt

Nat

ToInt

Internal (file)

Order (file)

Basic

Lemmas

MonadTail

Tactic

While

Meta (file)

Defs

Omega (file)

Coeffs

Constraint

Int

IntList

LinearCombo

Logic

Sym (file)

DSimp

DSimprocDSL

Simp

SimprocDSL

Lemmas

System (file)

CancelToken

FilePath

IO

IOError

Platform

Promise

ST

Uri

BinderNameHint

BinderPredicates

ByCases

CbvSimproc

Classical

Coe

Conv

Core

Dynamic

Ext

GetElem

Guard

Hints

LawfulBEqTactics

MacroTrace

MetaTypes

MethodSpecsSimp

Notation

NotationExtra

Prelude

PropLemmas

RCases

ShareCommon

SimpLemmas

Simproc

SizeOf

SizeOfLemmas

Syntax

Tactics

TacticsExtra

Task

Try

Util

WF

WFComputable

WFExtrinsicFix

WFTactics

While

Lake (file)

Build (file)

Job (file)

Basic

Monad

Register

Target (file)

Basic

Fetch

Actions

Common

Context

Data

Executable

ExternLib

Facets

Fetch

Index

Info

Infos

InitFacets

InputFile

Key

Library

Module

ModuleArtifacts

Package

Run

Store

Targets

Topological

Trace

CLI

Actions

Config (file)

Artifact

Cache

ConfigDecl

ConfigTarget

Context

Defaults

Dependency

Dynlib

Env

ExternLib

ExternLibConfig

FacetConfig

Glob

InputFile

InputFileConfig

InstallPath

Kinds

LakeConfig

Lang

LeanConfig

LeanExe

LeanExeConfig

LeanLib

LeanLibConfig

Meta

MetaClasses

Module

Monad

Opaque

OutFormat

Package

PackageConfig

Pattern

Script

TargetConfig

Workspace

WorkspaceConfig

DSL (file)

Attributes

AttributesCore

Config

DeclUtil

Extensions

Key

Meta

Package

Require

Script

Syntax

Targets

VerLit

Toml (file)

Data (file)

DateTime

Dict

Value

Elab (file)

Expression

Value

Decode

Encode

Grammar

Load

ParserUtil

Util (file)

Binder

Casing

Cli

Cycle

Date

EStateT

EquipT

Error

Exit

Family

FilePath

Git

IO

JsonObject

Lift

Lock

Log

MainM

Message

Name

NativeLib

Opaque

OpaqueType

OrdHashSet

OrderedTagAttribute

Proc

RBArray

Reservoir

Store

StoreInsts

String

Task

Url

Version

Reservoir

Version

Lean (file)

Compiler (file)

IR (file)

Basic

Checker

CompilerM

EmitLLVM

EmitUtil

Format

LLVMBindings

Meta

NormIds

Sorry

ToIR

ToIRType

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

CoalesceRC

CompatibleTypes

CompilerM

ConfigOptions

DeclHash

DependsOn

ElimDead

ElimDeadBranches

EmitC

EmitUtil

ExpandResetReuse

ExplicitBoxing

ExplicitRC

ExtractClosed

FVarUtil

FixedParams

FloatLetIn

InferBorrow

InferType

Internalize

Irrelevant

JoinPoints

LCtx

LambdaLifting

Level

LiveVars

Main

MonadScope

MonoTypes

OtherDecl

PassManager

Passes

PhaseExt

PrettyPrinter

Probing

PropagateBorrow

PublicDeclsExt

PullFunDecls

PullLetDecls

PushProj

ReduceArity

ReduceJpArity

Renaming

ResetReuse

ScopeM

SimpCase

SimpleGroundExpr

SpecInfo

Specialize

SplitSCC

StructProjCases

ToDecl

ToExpr

ToImpure

ToImpureType

ToLCNF

ToMono

Toposort

Types

Util

Visibility

BorrowedAnnotation

CSimpAttr

ClosedTermCache

ExportAttr

ExternAttr

FFI

ImplementedByAttr

InitAttr

InlineAttrs

Main

MetaAttr

ModPkgExt

NameDemangling

NameMangling

NeverExtractAttr

NoncomputableAttr

Old

Options

Specialize

Data (file)

Iterators (file)

Producers (file)

PersistentHashMap

Json (file)

FromToJson (file)

Basic

Extra

Basic

Elab

Parser

Printer

Stream

Lsp (file)

Basic

BasicAux

CancelParams

Capabilities

Client

CodeActions

Communication

Diagnostics

Extra

InitShutdown

Internal

Ipc

LanguageFeatures

TextSync

Utf16

Window

Workspace

NameMap (file)

AdditionalOperations

Basic

Array

AssocList

DeclarationRange

EditDistance

Format

FuzzyMatching

JsonRpc

KVMap

LBool

LOption

Name

NameTrie

OpenDecl

Options

PPContext

PersistentArray

PersistentHashMap

PersistentHashSet

Position

PrefixTree

RArray

RBMap

RBTree

SMap

SSet

Trie

DocString (file)

Add

Extension

Formatter

Links

Markdown

Parser

Syntax

Types

Elab (file)

BuiltinDo (file)

Basic

For

Forward

If

Jump

Let

Match

MatchExpr

Misc

Repeat

TryCatch

Command (file)

Scope

WithWeakNamespace

ConfigEval (file)

Basic

Builtins

Commands

DeriveEvalConfigItem

DeriveEvalExpr

DeriveEvalTerm

Extra

Instances

MetaInstances

Types

Util

Deriving (file)

BEq

Basic

DecEq

FromToJson

Hashable

Inhabited

LawfulBEq

Nonempty

Ord

ReflBEq

Repr

SizeOf

ToExpr

TypeName

Util

Do (file)

Basic

Control

ForwardSyntax

InferControlInfo

Legacy

PatternVar

Switch

DocString (file)

Builtin (file)

Keywords

Parsing

Postponed

Scopes

InfoTree (file)

InlayHints

Main

Types

PreDefinition (file)

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

EqnsUtils

FixedParams

Main

MkInhabitant

Mutual

TerminationHint

TerminationMeasure

Quotation (file)

Precheck

Util

Tactic (file)

BVDecide (file)

BVCheck

BVDecide

BVTrace

Normalize

Conv (file)

Basic

Cbv

Change

Congr

Delta

Lets

Pattern

Rewrite

Simp

Unfold

Do (file)

Internal (file)

VCGen (file)

Context

Driver

Entails

Frontend

Reduce

RuleCache

RuleConstruction

Solve

SpecDB

Util

ProofMode (file)

Assumption

Basic

Cases

Clear

Constructor

Delab

Exact

Exfalso

Focus

Frame

Have

Intro

LeftRight

MGoal

Pure

Refine

RenameI

Revert

Specialize

VCGen (file)

Basic

Split

SuggestInvariant

Attr

LetElim

Spec

Syntax

Grind (file)

Anchor

Annotated

Basic

BuiltinTactic

Config

DSimprocDSL

DSimprocDSLBuiltin

Filter

Have

Lint

LintExceptions

Main

Param

RegisterSymDSimp

RegisterSymSimp

ShowState

SimprocDSL

SimprocDSLBuiltin

Sym

Trace

WithGrindTacticM

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

AsAuxLemma

Basic

BoolToPropSimps

BuiltinTactic

Calc

Cbv

CbvSimproc

Change

Classical

Config

Congr

Decide

Delta

DiscrTreeKey

Doc

ElabTerm

ExposeNames

Ext

FalseOrByContra

Generalize

Guard

Impossible

Induction

Injection

Lets

LibrarySearch

Location

Match

Meta

Monotonicity

NormCast

RCases

RenameInaccessibles

Repeat

Rewrite

Rewrites

Rfl

Show

ShowTerm

Simp

SimpArith

SimpTrace

Simpa

Simproc

SolveByElim

Split

Symm

TreeTacAttr

Try

Unfold

Term (file)

TermElabM

App

Arg

AssertExists

Attributes

AutoBound

AuxDef

BinderPredicates

Binders

BindersUtil

BuiltinCommand

BuiltinEvalCommand

BuiltinNotation

BuiltinTerm

Calc

CheckTactic

Coinductive

ComputedFields

Config

DeclModifiers

DeclNameGen

DeclUtil

Declaration

DeclarationRange

DefView

DeprecatedArg

DeprecatedSyntax

ElabRules

ErrorExplanation

ErrorUtils

Eval

Exception

Extra

Frontend

GenInjective

GuardMsgs

Idbg

Import

Inductive

InfoTrees

InheritDoc

LetRec

Level

Macro

MacroArgUtil

MacroRules

Match

MatchAltView

MatchExpr

Mixfix

MutualDef

MutualInductive

Notation

Open

Parallel

ParseImportsFast

PatternVar

Print

RecAppSyntax

RecommendedSpelling

SetOption

StructInst

StructInstHint

Structure

Syntax

SyntheticMVars

Task

Time

Util

WhereFinally

Language

Lean (file)

Types

Basic

Util

LibrarySuggestions (file)

Basic

Default

MePo

SineQuaNon

SymbolFrequency

Linter (file)

EnvLinter (file)

Basic

Frontend

Extra (file)

DupNamespace

UnnecessarySeqFocus

UnreachableTactic

UnusedDecidableInType

Basic

Builtin

CheckUnivs

Coe

ConstructorAsVariable

DefProp

Deprecated

DocsOnAlt

GlobalAttributeIn

Init

List

MissingDocs

Omit

PersistentLintLog

Sets

TacticTypeCheck

UnusedSimpArgs

UnusedVariables

Util

Meta (file)

ArgsPacker (file)

Basic

Constructions (file)

BRecOn

CasesOn

CasesOnSameCtor

CtorElim

CtorIdx

NoConfusion

RecOn

SparseCasesOn

SparseCasesOnEq

DiscrTree (file)

Basic

Main

Types

Util

Match (file)

MatcherApp (file)

Basic

Transform

AltTelescopes

Basic

CaseArraySizes

CaseValues

MVarRenaming

Match

MatchEqs

MatchEqsExt

MatchPatternAttr

MatcherInfo

NamedPatterns

Rewrite

SimpH

SolveOverlap

Value

Sym (file)

Arith (file)

Classify

DenoteExpr

EvalNum

Functions

MonadCanon

MonadRing

MonadSemiring

MonadVar

Poly

Reify

ToExpr

Types

VarRename

DSimp (file)

App

DSimpM

DSimproc

EvalGround

Forall

Lambda

Let

Main

Reduce

Result

Variant

Simp (file)

App

Attr

CongrInfo

ControlFlow

Debug

Discharger

DiscrTree

EvalGround

Forall

Goal

Have

Lambda

Main

RegisterCommand

Result

Rewrite

SimpM

Simproc

Telescope

Theorems

Variant

AbstractS

AlphaShareBuilder

AlphaShareCommon

Apply

Canon

Eta

ExprPtr

Grind

InferType

InstantiateMVarsS

InstantiateS

Intro

IsClass

LitValues

LooseBVarsS

MaxFVar

Offset

Pattern

ProofInstInfo

ReplaceS

SymM

SynthInstance

Util

Tactic (file)

AC (file)

Main

BVDecide (file)

LRAT (file)

Cert

Trim

Normalize (file)

AC

AndFlatten

ApplyControlFlow

Basic

EmbeddedConstraint

Enums

IntToBitVec

Rewrite

ShortCircuit

Simproc

Structures

TypeAnalysis

Prover (file)

Basic

Bitblast

Reflect (file)

Basic

ReifiedBVExpr

ReifiedBVLogical

ReifiedBVPred

ReifiedLemmas

Reify

SatAtBVLogical

Attr

Counterexample

External

Main

TacticContext

Cbv (file)

BuiltinCbvSimprocs

Array

Core

String

CbvEvalExt

CbvSimproc

ControlFlow

Main

Opaque

TheoremsLookup

Util

Grind (file)

AC (file)

Action

DenoteExpr

Eq

Internalize

Inv

PP

Proof

Seq

ToExpr

Types

Util

Var

VarRename

Arith (file)

CommRing (file)

Action

DenoteExpr

EqCnstr

Functions

Internalize

Inv

MonadRing

MonadSemiring

NonCommRingM

NonCommSemiringM

PP

Power

Proof

Reify

RingId

RingM

SafePoly

SemiringM

Types

Cutsat (file)

Action

CommRing

DvdCnstr

EqCnstr

Inv

LeCnstr

MBTC

Model

Nat

Norm

Proof

ReorderVars

Search

SearchM

ToInt

ToIntInfo

Types

Util

Var

VarRename

Linear (file)

Action

Den

DenoteExpr

IneqCnstr

Internalize

Inv

LinearM

MBTC

Model

OfNatModule

PP

Proof

PropagateEq

Reify

Search

SearchM

StructId

ToExpr

Types

Util

Var

VarRename

EvalNum

FieldNormNum

Insts

IsRelevant

Main

Model

ModelUtil

Propagate

Simproc

Types

Util

Order (file)

Assert

Internalize

OrderM

Proof

StructId

Types

Util

Action

Anchor

Attr

Beta

Cases

CasesMatch

CastLike

CheckResult

CollectParams

Core

Ctor

CtorIdx

Diseq

EMatch

EMatchAction

EMatchTheorem

EMatchTheoremParam

EMatchTheoremPtr

EqResolution

Ext

ExtAttr

Extension

Filter

Finish

ForallProp

Injection

Injective

Internalize

Intro

Inv

LawfulEqCmp

Lookahead

MBTC

Main

MarkNestedSubsingletons

MatchCond

MatchDiscrOnly

OrderInsts

PP

Parser

Proj

Proof

ProofUtil

Propagate

PropagateInj

PropagatorAttr

ProveEq

ReflCmp

RegisterCommand

RevertAll

Simp

SimpUtil

Solve

Split

SynthInstance

Theorems

Types

Util

VarRename

Simp (file)

Arith (file)

Int (file)

Basic

Simp

Nat (file)

Basic

Simp

Util

BuiltinSimprocs (file)

Array

BitVec

Char

Core

CtorIdx

Fin

Int

List

MethodSpecs

Nat

SInt

String

UInt

Util

Attr

Diagnostics

LoopProtection

Main

RegisterCommand

Rewrite

SimpAll

SimpCongrTheorems

SimpTheorems

Simproc

Types

Try (file)

Collect

Acyclic

Apply

Assert

Assumption

AuxLemma

Backtrack

Cases

CasesOnStuckLHS

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

CasesInfo

Check

CheckTactic

Closure

Coe

CoeAttr

CollectFVars

CollectMVars

CompletionName

CongrTheorems

CtorIdxHInj

CtorRecognizer

DecLevel

Diagnostics

Eqns

Eval

ExprDefEq

ExprLens

ExprTraverse

ForEachExpr

FunInfo

GeneralizeTelescope

GeneralizeVars

GetUnfoldableConst

HasAssignableMVar

HasNotBit

HaveTelescope

Hint

IndPredBelow

Inductive

InferType

Injective

Instances

IntInstTesters

Iterator

KAbstract

KExprMap

LazyDiscrTree

LetToHave

LevelDefEq

LitValues

MatchUtil

MethodSpecs

MkIffOfInductiveProp

MonadSimp

NatInstTesters

NatTable

Native

Offset

Order

PPBinder

PPGoal

PProdN

ProdN

RecExt

RecursorInfo

Reduce

ReduceEval

SameCtorUtils

SizeOf

Sorry

SplitSparseCasesOn

StringLitProof

Structure

SynthInstance

Transform

TransparencyMode

TryThis

UnificationHint

WHNF

WrapInstance

Parser (file)

Module (file)

Syntax

Tactic (file)

Doc

Term (file)

Basic

Doc

Attr

Basic

Command

Do

Extension

Extra

Level

StrInterpolation

Syntax

Types

ParserCompiler (file)

Attribute

PrettyPrinter (file)

Delaborator (file)

Attributes

Basic

Builtins

DeclWithSig

FieldNotation

Metavariable

Options

SubExpr

TopDownAnalyze

Basic

Formatter

Parenthesizer

Server (file)

CodeActions (file)

Attr

Basic

Provider

UnknownIdentifier

Completion (file)

CompletionCollectors

CompletionInfoSelection

CompletionItemCompression

CompletionResolution

CompletionUtils

EligibleHeaderDecls

ImportCompletion

SyntheticCompletion

FileWorker (file)

ExampleHover

InlayHints

RequestHandling

SemanticHighlighting

SetupFile

SignatureHelp

Utils

WidgetRequests

Rpc (file)

Basic

Deriving

RequestHandling

Test (file)

Cancel

Refs

Runner

AsyncList

FileSource

GoTo

InfoUtils

Logging

ProtocolOverview

References

RequestCancellation

Requests

ServerTask

Snapshots

Utils

Watchdog

Util (file)

CollectAxioms

CollectFVars

CollectLevelMVars

CollectLevelParams

CollectLooseBVars

CollectMVars

Diff

FVarSubset

FindExpr

FindLevelMVar

FindMVar

FoldConsts

ForEachExpr

ForEachExprWhere

HasConstCache

Heartbeats

InstantiateLevelParams

LakePath

LeanOptions

MonadBacktrack

MonadCache

NumApps

NumObjs

OccursCheck

PPExt

ParamMinimizer

Path

Profile

Profiler

ProfilerServer

PtrSet

RecDepth

Recognizers

ReplaceExpr

ReplaceLevel

Reprove

SCC

SafeExponentiation

ShareCommon

Sorry

SortExprs

TestExtern

Trace

UnusedBinders

Widget (file)

Basic

Commands

Diff

InteractiveCode

InteractiveDiagnostic

InteractiveGoal

TaggedText

Types

UserWidget

AddDecl

Attributes

AutoDecl

AuxRecursor

BuiltinDocAttr

Class

CompactedRegion

CoreM

Declaration

DeclarationRange

DefEqAttrib

DeprecatedModule

EnvExtension

Environment

ErrorExplanation

Exception

Expr

ExtraModUses

HeadIndex

Hygiene

IdentifierSuggestion

ImportingFlag

InternalExceptionId

KeyedDeclsAttribute

LabelAttribute

Level

LoadDynlib

LocalContext

Log

Message

MetavarContext

Modifiers

MonadEnv

Namespace

OriginalConstKind

PrivateName

ProjFns

ReducibilityAttrs

Replay

ReservedNameAction

ResolveName

Runtime

ScopedEnvExtension

Setup

Shell

Structure

SubExpr

Syntax

ToExpr

ToLevel

LeanPool (file)

ABCExceptions (file)

ForMathlib (file)

RingTheory (file)

Radical

Misc

Section2

Section4

AFormalizationOfBorelDeterminacyInLean (file)

Applications (file)

Choquet

General

Meager

RegularOpen

Basic (file)

FinLists

General

InfLists

InvLimitNat

Meta

MiscCat

Game (file)

BuildStrategies

GaleStewart

Games

Player

Strategies

Undetermined

Proof (file)

One (file)

Lift

PreLift

Strat

Zero (file)

Lift

PreLift

Strat

TreeLift

BorelDeterminacy

BuildLevelwise

Covering

CoveringClosedGame

CoveringLim

WinAsap

Tree (file)

BodyFunctor

LenTreeHom

PointedTrees

RestrictTree

TreeBody

TreeExtensions

TreeLim

Trees

QualityAliases

AgreeToDisagree (file)

AgreeToDisagree

AgreeToDisagreeBeliefs

AharoniKorman (file)

ForMathlib (file)

Misc

Counterexample

AndersonConjecture (file)

CompleteDomain (file)

CompleteDomain

Domain

LocalRing

Jensen (file)

Adjoin (file)

Adjoin

FromPrime

Transcendental

CloseUp (file)

AvoidanceStep

Base

CloseUp

CoprimeSplit

Factor

FactorDivisibility

GcdComplexity

IntersectionHelpers

IntersectionStep

NoCommonFactor

TwoGen

Construction (file)

ChainHelpers

Construction

HeitmannProp

Transfinite

KrullDomain (file)

AdjoinLocSet

HeightBound

KrullDomain

LocUFD

Nagata

Prime

UFDConstruction

Application

Avoidance

CombinedStep

Defs

Jensen

NSubring

TransfiniteUnion

QuasiCompleteRing (file)

Complete

QuasiCompleteRing

AdicKerEval

AdicLocal

AdicNoetherian

Basic

Main

Apportionment (file)

Basic

PlausibleInstances

Utils

ArchonFirstProofResults (file)

FirstProof4 (file)

Auxiliary (file)

BoxPlusRealRoots

Continuity

Defs

Density

HarmonicBound

InvPhiN

Obreschkoff

ObreschkoffTransport

PhiN

RPoly

RealRoots

Residue

RootContinuity

SignSquarefree

Transport

TransportDecomp

Problem4

FirstProof6 (file)

Auxiliary (file)

BarrierPotential

ColoringFramework

DynamicColoring

LaplacianBasics

LoewnerPullback

OneSidedBarrier

ResolventBound

Problem6

ArtinWedderburn (file)

ArtinWedderburnTheorem

Auxiliary

CornerCornerLemma

CornerRing

IdealProd

Idempotents

MatrixUnits

MinIdeals

NiceIdeals

NonUnitalToUnital

PrimeRing

SetProd

Biswal (file)

Theorem1

Theorem23

BrauerGroupNew (file)

Azumaya

Basic

Mul

Examples

ShortComplex

LeftHomologyMapData

Mathlib (file)

Algebra (file)

Algebra (file)

Subalgebra (file)

Basic

Directed

Lattice

Equiv

Data (file)

DFinsupp (file)

Submonoid

LinearAlgebra (file)

LinearIndependent (file)

Defs

Matrix (file)

Charpoly (file)

Basic

GeneralLinearGroup (file)

Basic

Span (file)

Basic

RepresentationTheory (file)

Homological (file)

GroupCohomology (file)

LowDegree

RingTheory (file)

Congruence (file)

Basic

Defs

NonUnitalSubring (file)

Defs

NonUnitalSubsemiring (file)

Basic

Defs

TensorProduct (file)

Basic

TwoSidedIdeal (file)

Basic

Kernel

Lattice

Operations

MatrixAlgebra

Morita

ChangeOfRings

TensorProduct

Subfield (file)

Defs

FiniteDimensional

Separable

Splitting

Subfield

AbsoluteIsoH2

AlgClosedUnion

BrauerGroup

BrauerOverR

CentralSimple

Centralizer

CrossProductAlgebra

DoubleCentralizer

ExtendScalar

FieldCat

FiniteField

FrobeniusTheorem

IsoSecond

LemmasAboutSimpleRing

MatrixCenterEquiv

MatrixEquivTensor

MoritaEquivalence

RelativeBrauer

SkolemNoether

SplittingOfCSA

ToSecond

TwoSidedIdeal

Wedderburn

ZeroSevenFourE

Brouwer (file)

Brouwer

BrouwerProduct

Nash

Primitive

Scarf

ScarfPath

Simplex

BruhatTits (file)

Cartan (file)

Existence

Uniqueness

Graph (file)

Edges

Graph

GroupAction

Orientation

Regular

Tree

Vertices

Harmonic (file)

Application

Basic

Lattice (file)

Basic

Construction

Distance

Quotient

Transvect

Utils (file)

GLSubmoduleAction

GraphAction

LinearAlgebra

List

Matrix

Misc

Order

RingHom

Subring

ValuationRings

Burkholder (file)

Majorants (file)

Definitions

MajorantPEq2

MajorantPG2

MajorantPL2

MartingaleTransforms

CencovPetz (file)

Basic

CencovFinite

CencovSplitPoint

ContinuousExtension

FisherContinuity

LeftInverseIsometry

MarkovMorphism

MonotoneMetric

PermutationInvariance

PermutationInvariantBilinForm

RationalDensity

RationalPoint

Replication

ReplicationInvariance

Simplex

SimplexTopology

Splitting

SplittingInvariance

SplittingUniform

SufficientStatistic

Uniform

UniformScalarConstant

UniformScalarMultiple

UniformSimplex

CircuitComplexity (file)

AC0 (file)

Defs

AON (file)

Defs

Digraph

Defs

Internal

AON

Bridge

CircDesc

LowerBound

NF

Nondeterminism

Schnorr

ShannonUpper

Simulation

Valiant

NF (file)

Defs

Nondeterminism (file)

Defs

Basic

EssentialInput

LowerBound

Schnorr

Shannon

Valiant

XOR

Circuitlib (file)

Circuit

Belnap

Basic

Gate

Level

Category

Basic

Combinational

Sequential

Basic

Combinational

Gate

Wires

Clawristotle (file)

CoulombConcreteTheorem42

CoulombFlux

CoulombFluxBound

CoulombFluxConv

CoulombFluxDiff

CoulombForceTransport

CoulombKernel

CoulombNonvacuous

CoulombPSD

CoulombPSDHelpers

CoulombSpatialTransport

Defs

FlatTorus3Lemmas

GaussianHelpers

IteratedDerivHelpers

LogBoundHelpers

NewtonianPotential

SchwartzDecayDefs

Section2

Section3

Section3Helpers

Section3Helpers2

Section4

Section5

Section6

Section7

Section8

Theorem42

TorusDefs

TorusInstance

TorusIntegration

VMLInputDerive

VMLStructures

VelocityDecayInstance

CompactSpectral (file)

Analysis

InnerProductSpace

CompactSelfAdjoint (file)

Approximation

Basic

CutoffProjector

OpNormEigenvalue

SpectralFiniteness

SpectralTheorem

CompactOperatorOrthonormal

RayleighCompact

Topology

WeakHilbertCompact

Computability (file)

ArithHierarchy

AutGrp

Encoding

Jump

Oracle

TuringDegree

ComputableReal (file)

SpecialFunctions (file)

Basic

Exp

Pi

Sqrt

AuxLemmas

ComputableRSeq

ComputableReal

IsComputable

IsComputableC

ConnesKreimer (file)

Coassoc

Core

PowerSeriesLogMul

CriticalPortraits (file)

Census

Core

CycleLemma

Denominator

Forward

Injectivity

Portraits

Surjectivity

DeadEnds (file)

Basic

CRT

Counting

CountingBlocks

InclusionExclusion

PrimeTail

RelevantPrimes

Solution

TailEstimates

DemazureOperatorsLean (file)

Demazure

DemazureAux

DemazureAuxRelations

DemazureRelations

Matsumoto

StrongExchange

DemazureProduct (file)

AspPerm

Avoiding321

InvSet

ReducedProducts

Reduction

SlipFace

Submodular

Tableaux

Transpositions

Utils

Valley

Desargues (file)

Basic

Morphism

PV

Structure

DirectedTopologyLean4 (file)

SplitPath (file)

SplitDipath

SplitPath

SplitProperties

Constructions

CoverLemma

DTop

DihomotopyCover

DihomotopyFlip

DihomotopyToPathDihomotopy

Dipath

DipathSubtype

DirectedHomotopy

DirectedMap

DirectedPathHomotopy

DirectedSpace

DirectedUnitInterval

DirectedVanKampen

Fraction

FractionEqualities

FundamentalCategory

Interpolate

MonotonePath

MorphismAux

PathCover

PushoutAlternative

SplitDihomotopy

StretchPath

TransRefl

UnitIntervalAux

DomainTheory (file)

ContinuousLattice

Constructions

FunctionSpaceTower

FunctionSpaces

Injective

InverseLimits

MilnerCorrection

ScottMaps

Specialization

Theorem212

WayBelow

Neighborhood

Approximable

ApproximableExercises

Basic

Definition610

Definition613

Definition63

Definition68

Definition71

Definition72

Example12

Example13

Example14

Example15

Example23

Example24

Example43

Example44

Example61

Example62

Example62A

Example62C

Example62Regular

ExampleB

Exercise112

Exercise113

Exercise114

Exercise115

Exercise116

Exercise117

Exercise118

Exercise119

Exercise120

Exercise121

Exercise122

Exercise123

Exercise124

Exercise125

Exercise126

Exercise127

Exercise213

Exercise214

Exercise215

Exercise216

Exercise218

Exercise220

Exercise221

Exercise222

Exercise314

Exercise315

Exercise316

Exercise317

Exercise318

Exercise319

Exercise319Sum

Exercise321

Exercise322

Exercise323

Exercise324

Exercise324Distrib

Exercise324Iter

Exercise325

Exercise326

Exercise326Sum

Exercise327

Exercise328

Exercise407

Exercise408

Exercise409

Exercise410

Exercise411

Exercise412

Exercise413

Exercise414

Exercise415

Exercise416

Exercise417

Exercise418

Exercise419

Exercise420

Exercise421

Exercise422

Exercise423

Exercise424

Exercise425

Exercise507

Exercise508

Exercise509

Exercise510

Exercise511

Exercise512

Exercise513

Exercise514

Exercise515

Exercise516

Exercise516Overlap

Exercise516ThueMorse

Exercise617

Exercise617Gen

Exercise618

Exercise619

Exercise619PartB

Exercise621

Exercise622

Exercise623

Exercise624

Exercise625

Exercise626

Exercise627

Exercise628

Exercise629

FunctionSpace

Lemma615

Product

Proposition53

Proposition54

Proposition611

Proposition612

Proposition66

Proposition67

Proposition77

Recursive

Table55

Theorem110

Theorem111

Theorem41

Theorem46

Theorem51

Theorem52

Theorem56

Theorem56Full

Theorem614

Theorem616

Theorem69

Theorem74

Theorem75

Theorem76

Constructive

InfoSys

Duality (file)

Common

ExtendedFields

FarkasBartl

FarkasBasic

FarkasSpecial

LinearProgramming

LinearProgrammingB

EcTateLean (file)

Algebra

CharP

Basic

EllipticCurve

AuxRingLemmas

KodairaTypes

Kronecker

Model

Ring

Basic

FieldTheory

PerfectClosure

Init

Data

Int

Lemmas

Egrs75 (file)

AddBranch

BadPrefixRoute

CentralBinomialDigits

ClearingHigh

ConditionThreeWindow

Defs

DigitAtToolkit

DigitVector

Instances

KummerValuation

LeafInduction

LogIrrationality

MoveDigits

MuFinish

Reduction

RoundUp

SeedWindow

SubtractBranch

Erdos1196 (file)

Basic

FirstEntryRowTerm

FormalConjecturesErdos1196

HitMass

Main

Markov

Normalization

NormalizationCore

NormalizationSmallPrime

Preliminaries

PreliminariesMertens

PreliminariesTailAux

PrimitiveWeight

Erdos137 (file)

AxiomAudit

Base

BlockFramework

CombinedSplice

Finiteness

JointFiniteness

QuarticCrude

RefinedOverlap

RoughPartStructure

SexticCrude

SmoothRefinement

SpliceFiniteness

SquarefreeCapacity

TaoPoint

Erdos367 (file)

Core139

Core4027

GeneralKUpperBound

K3AbcUpperBound

PellLimsup

RFullLowerBound

Erdos403 (file)

Basic

FactBase

Sharp

ErdosTuzaValtr (file)

Config

Default

Defs

Lemmas

Mirror

Etv

AlphaBeta

Default

Defs

Label

Mirror

Lib

Core

Rel3

List

Chain3

Default

Defs

Lemmas

Main

Lemmas

Default

InterweavedLacedNgon

JoinN2N2

JoinN2N3JoinN3N2

JoinN2N3N2

CapCup

Defs

InductionStep

Main

All

EventStructures (file)

Basic

Computation

Configuration

FinitePoset

Log

Path

Replay

Rollback

Trace

FactorizationSystems (file)

Basic

Characterization

Examples

OrthogonalComplements

Orthogonality

FelConjecture (file)

Solution

Fineqs (file)

Main

FiveEighthsTheorem (file)

Basic

Flean (file)

Basic

FloatCfg

FloatRep

IntRounding

LogRules

Rounding

Subnorm

FoZfc (file)

Axioms

Basic

BoundedFormulaOps

FixedSnoc

Replacement

Tostring

FormalLearningTheory (file)

Complexity (file)

Generalization (file)

Core

Tail

Amalgamation

BorelAnalyticBridge

Compression

DualVC

FiniteSupportUC

GameInfra

GeneralizationResults

Interpolation

Littlestone

Measurability

MindChange

Ordinal

Rademacher

Structures

Symmetrization

VCDimension

Criterion (file)

Extended

Gold

Online

PAC

Learner (file)

Active

Bayesian

Closure

Core

Monad

Properties

VersionSpace

PureMath

AnalyticMeasurability

ApproxMinimax

BinaryMatrix

ChoquetCapacity

Concentration

Exchangeability

FiniteVCApprox

KLDivergence

ReaderMonad

Theorem (file)

BorelAnalyticSeparation

Extended

Gold

Online

PAC

PACBayes

Separation

Basic

Bridge

Computation

Data

Process

FormalizationOfBoundedArithmetic (file)

Algebra

AxiomSchemes

BasicSingleSorted

Complexity

DisplayedVariables

IDelta0

IOPEN

IsEnum

LanguagePeano

LanguageZambella

MathlibSimps

Order

Register

Semantics

SimpRules

Syntax

V0

V0StrAddAssoc

V0StrAddComm

V0StrSuccAssoc

ForwardEuler (file)

Main

FriezePatterns (file)

Chapter1

Chapter2

Chapter3

FrontierMathOpenHypergraphs (file)

Uniform (file)

FrameBoosters

FrameDefs

FrameExact

FrameResidues

Frames

Basic

Lubell

Substitution

GrothendieckVanishing (file)

ClosedImmersion

ClosedImmersionCohomology

CohomologyAPI

ConstantSheafFlasque

FinitelyGeneratedVanishing

FlasqueVanishing

GeneratedSubsheaf

GrothendieckVanishing

GrothendieckVanishingOverview

IrreducibleStep

PresheafFilteredColimit

PresheafFilteredColimitCore

PresheafFilteredColimitGeneral

TopologicalKrullDim

ZeroOutside

HSDInteriorPointLP (file)

FixedYTMTheory

GeneratedConvergence

LocalNeighborhoodEstimates

NewtonSystem

PrimalDualData

Incompleteness (file)

Arith

D1

D3

DC

First

FormalizedArithmetic

Second

Theory

Arithmetization

Basic

IOpen

Ind

PeanoMinus

Definability

Absoluteness

Boldface

BoundedBoldface

Hierarchy

Init

ISigmaOne

HFS (file)

Basic

Coding

Fixpoint

PRF

Seq

Vec

Metamath (file)

Formula

Basic

Functions

Iteration

Typed

Proof

Derivation

Thy

Typed

Term

Basic

Functions

Typed

CodedTheory

Coding

Language

Bit

ISigmaZero

Exponential

Exp

Log

PPow2

Pow2

Vorspiel

ExistsUnique

Graph

Lemmata

Vorspiel

DC

Basic

Foundation

FirstOrder

Arith

Basic

CobhamR0

Hierarchy

Model

PeanoMinus

Representation

StrictHierarchy

Theory

Basic (file)

Semantics

Elementary

Semantics

Syntax

Formula

Rew

BinderNotation

Calculus

Calculus2

Coding

Eq

Model

Operator

Soundness

Completeness

Coding

Completeness

Corollaries

SearchTree

SubLanguage

Order

Le

Ultraproduct

IntProp

Hilbert

Basic

Int

WellKnown

Kripke

Hilbert

Cl

Basic

Classical

Soundness

Basic

Formula

Substitution

Logic

HilbertStyle

Basic

Context

Lukasiewicz

Supplemental

Predicate

Language

Quantifier

Rew

Term

Axioms

Calculus

Disjunctive

Entailment

LogicSymbol

Semantics

Modal

Entailment

Basic

GL

Grz

K

K4

K5

KD

KP

KT

KTc

S5

Triv

Hilbert

Maximal

Basic

Unprovability

Basic

Geach

K

S5Grz

WellKnown

Kripke

Hilbert

GL

Completeness

MDP

Soundness

Tree

Unnecessitation

Grz

Completeness

Soundness

Geach

K

K4

K45

K5

KB

KB4

KB5

KD

KD4

KD45

KD5

KDB

KT

KT4B

KTB

S4

S4Dot2

S4Dot3

S5

Soundness

Triv

Ver

AxiomDot3

AxiomGrz

AxiomL

AxiomVer

Basic

Closure

Completeness

Filteration

FiniteFrame

KHIncompleteness

Preservation

SimpleExtension

Tree

Logic

Basic

WellKnown

Axioms

Complement

ComplementClosedConsistentFinset

Formula

Geachean

IntProp

LogicSymbol

MaximalConsistentSet

Subformulas

Substitution

Vorspiel

Arith

BinaryRelations

Chain

Collection

ExistsUnique

NotationClass

Order

RelItr

Vorspiel

ProvabilityLogic

Basic

ToFoundation

Basic

IsTranscendentalPi (file)

AnalyticEstimates

CalculusOnPoly

ComplexExponential

IncrementalDerivatives

Main

NivenPolynomials

ScaledAuxiliaryPolynomial

SubsetSumPolynomial

SymmetricPolynomials

Isoperimetric (file)

Basic

BrunnMinkowski

Isoperimetric

PrekopaLeindler

KaltonRoberts (file)

Collections

Defs

DualCert

EpsilonRecombination

Intersections

Lemmas

LogBounds

MainTheorem

Numerical

PhiAnalysis

PhiDeriv

Pipeline

PipelineEps

Pippenger

PippengerProof

Recombination

UniformRecombination

KrafftSieve (file)

Basic

Defs

MainTheorem

OptimalWeights

SelbergWeights

ThirdHarmonic

Variance

LatticeTriangle (file)

Solution

Lean4GlCoalgebras (file)

General

Completeness

Game

Proof

Soundness

Interpolation

Interpolants

Interpolation

PartialInterpolation

Logic

FixedPointTheorem

Semantics

Syntax

Pdl

Game

Split

Completeness

CutProof

Game

Proof

ProofTransformations

Soundness

Lean4Itree (file)

ITree (file)

Basic

EffectAlgebra

Monad

Utils

Paco (file)

Paco

PacoDefs

PacoTactics

LeanBooleanfun (file)

ToMathlib (file)

Finset

Arrow

AuxLemmas

Basic

BooleanValued

LeanComplexAnalysis (file)

Harmonic (file)

Positive (file)

HarnackIneq

HerglotzRieszRepresentations

HerglotzRieszUnique

PoissonIntegral

PoissonIntegral2

PoissonIntegralCircleAverage

UnivalentFunctions (file)

ClassS

LeanModelChecking (file)

ABW

ABWNBW

LTLNBWResult

LTLNBWStatement

LTLNNF

NNFABW

SafetyLivenessDecomposition

LeanModularForms (file)

ContourIntegral

CrossingLimit

PVSplit

SegmentFTC

WindingNumber

ForMathlib

AtImInfty

Bounds

CongruenceSubgroupsCopy

CongruenceSubgrps

FunctionsBoundedAtInfty

Hassumunifon

Identities

Instances

IsBoundedAtImInfty

LevelOne

Petersson

QExpansion

SlashActions

UpperHalfPlane

GeneralizedResidueTheory

HomologicalCauchy (file)

Basic

DixonProof

Meromorphic

Homotopy

CircleParam

Integrality

Invariance

MathlibBridge

ParametricDiff

OnCurvePV

Basic

PVInfrastructure

AnnulusBounds

GammaAnalysis

RemainderAnalysis

SingularAnnulus

StepBounds

UniformStepBound

Residue (file)

FlatnessTransfer (file)

PerTermVanishing (file)

CPVHelpers

BoundaryVanishing

CPVExistence

CutoffInfrastructure

HigherOrderAssembly

MultipointPV (file)

DominatedConvergence

Flatness

GeneralizedTheorem

GeneralizedTheoremBase

MathlibBridge

MeasureHelpers

MeromorphicLaurent

MeromorphicPrincipalPart

SectorCurve

SectorCurveLemma

WindingNumber (file)

CrossingAnalysis

Decomposition

Defs

Proposition22

ArcCalculus

Basic

Bridges

CauchyPrimitive

CurveAvoidance

Cycle

GeneralizedResidueTheorem

LogDerivFTC

PiecewiseCurveAPI

PrincipalValue

HeckeRIngs

AbstractHeckeRing (file)

Associativity

Basic

Commutativity

Degree

Module

Multiplication

Ring

GL2

Basic

CongruenceIndex

Degree

HeckeAction

HeckeModularForm

MultiplicationTable

GLn

Basic

CoprimeMul

CosetDecomposition

Degree

DiagonalCosets

PolynomialRing

PrimeDecomposition

SLnTransvection

TransposeAntiInvolution

Modularforms

Generators (file)

Defs

Injectivity

Surjectivity

AtImInfty

BigO

Cauchylems

ClogArgLems

Cotangent

Csqrt

Delta

Derivative

DimensionFormulas

E2

Eisenstein

EisensteinAsymptotics

Eisensteinqexpansions

Equivs

Eta

EtaCleanup

ExpLems

ForMathlibCusps

ForMathlibFunctionsBoundedAtInfty

ForMathlibSlashActions

ForMathlibUpperHalfPlane

IccIcoLems

IsCuspForm

Iteratedderivs

JacobiTheta

LimunderLems

LogDerivLems

MDifferentiableFunProp

MultipliableLems

PhiTransform

QExpansion

QExpansionLems

RamanujanIdentities

ResToImagAxis

RiemannZetalems

SerreDerivativeSlash

SlashActionAuxil

SummableLems

Tendstolems

ThetaDerivIdentities

TsumderivWithin

Uniformcts

Upperhalfplane

SpherePacking

CuspDecay

PhiHolomorphic

ViazovskaMagicFunction

ValenceFormula

Boundary

Winding

Framework

LeftEdge

RightEdge

UnitArc

UnitArcHelpers

Basic

Bounds

Smooth

OnCurvePV

Basic

EndpointCorner

Main

PVChain (file)

Assembly (file)

ResidueSide

ArcContribution

Helpers

OnCurveCapture

ResidueSideInfra

Seg5CuspIntegral

RectHomotopy

AngleAnalysis

BoundaryHomotopyDerivBounds

BoundaryHomotopyDiff

BoundaryHomotopySmooth

Geometry

HomotopyDef

MainTheorem

MainTheoremBound

MainTheoremDerivCont

PolygonProps

PolygonSlope

RadialHomotopy

WindingBase

WindingProof

WindingWeights (file)

Common

I

Rho

RhoPlusOne

CoreIdentity

Definitions

InteriorWinding

ModularInvariance

OrbitPairing

OrbitSum

TextbookExistence

TextbookForm

TrigLemmas

LeanPolyABC (file)

Corollaries

Davenport

FltCatalan

NoParametrization

Lib

DivRadical

Max3

Radical

Wronskian

All

MasonStothers

LeanQuantumAlg (file)

Algorithms (file)

AmplitudeEstimation

BernsteinVazirani

DeutschJozsa

GHZ

Grover

OrderFinding

QPE

Simon

SuperdenseCoding

Teleportation

Core (file)

Components (file)

Control

Gates

Kets

Oracle

Cost

Gate

Measurement

State

Tensor

Primitives (file)

QKernel (file)

Advantage

Concentration

DiscreteLogConcept

Expressivity

Fidelity

Fourier

QNN (file)

DynamicalLieAlgebra

FullDLABasis

LieAlgebraicBP

Overparametrization

PauliPropagation

Trainability

VarianceFormula

QSP (file)

Chebyshev

Fourier

AmplitudeAmplification

BellPair

ControlledTransform

HadamardTest

LCU

ParameterShift

PhaseKickback

QFT

SwapTest

WalshHadamard

Util (file)

Complex

Concentration

FinPow

HilbertSchmidt

Polynomial

TrigPolynomial

Init

Lentil (file)

Gadgets

TheoremDeriving

TheoremLifting

ProofMode

Tactics (file)

Apply

Assumption

CheckGoalForm

Clear

CoalesceToPTL

Contradiction

Exists

Exit

Have

Intro

LeftRight

ModalityMisc

Monotone

Normalize

PurePred

RCases

Rename

Revert

Rewrite

Simp

Specialize

SplitAnds

Start

Basic

Display

Location

Rules

Basic

BigOp

LeadsTo

StatePred

WF

Tactics

Basic

FiniteWindow

Utils

MetaUtil

MiscLemmas

SyntaxUtil

Basic

Expr

Foldable

Util

LowDimSolvClassification (file)

Classification1

Classification2

Classification3

GeneralResults

InstancesConstructions

InstancesLowDim

LemmasDim3

QuotientSolvable

Semidirect

Tactics

MRiscX (file)

AbstractSyntax

AbstractSyntax

Instr

MState

Map

Delab

DelabCode

DelabHoare

Elab

CodeElaborator

HandleExpr

HandleNumOrIdent

HoareElaborator

Examples

Examples

OtpProof

SingleProofsOTP

SpecAutomation

Hoare

EvalLabelInHoare

HoareAssignmentElab

HoareCore

HoareRules

HoareTheory

Parser

AssemblySyntax

HoareSyntax

Semantics

MsTheory

Run

Specification

Tactics

ApplySpec

CodeProofTactics

GeneralCustomTactics

HelpCodeProofTactics

SpecificationTactics

SplitLastSeq

TacticUtil

Util

BasicTheorems

Basic

MisereGames (file)

AugmentedForm (file)

Lift

Short

Form (file)

Misere

Adjoint

Outcome

Adjoint

Birthday

Classes

Short

GameForm (file)

Birthday

Special

Literature

OnSumsOfPFreeFormsUnderMiserePlay

Mathlib

NatOrdinal

SimpleGraph

Small

Misere

Hereditary

MaintenanceProviso

OutcomeStable (file)

PropertyX

Ambient

Blocking

Closures

Comparison

DeadEnding

IntegerInvertible

LiftIncomparable

NonInvertible

Normal

PFree

PFreeBlocking

PFreeDeadEnding

Preservation

Quotients

Separation

ShortIncomparable

Stride

TippingPoints

Universe

Ruleset (file)

Hackenbush

Push

Shove

Strip

Tactic

DocAlias

GameGraph

OfSets

Outcome

Player

Monlib4 (file)

LinearAlgebra (file)

Coalgebra (file)

FiniteDimensional

Lemmas

MulOpposite

Ips (file)

Basic

Frob

Functional

Ips

MatIps

MinimalProj

MulOp

Nontracial

OpUnop

Pos

RankOne

Strict

Symm

TensorHilbert

Vn

Matrix (file)

Basic

Cast

Conj

IncludeBlock

IsAlmostHermitian

PiMat

PosDefRpow

PosEqLinearMapIsPositive

Reshape

Spectra

StarOrderedRing

QuantumSet (file)

Basic

DeltaForm

Instances

PhiMap

Pi

QIso

SchurMul

SchurMulTensor

Subset

Symm

TensorProduct

TensorProduct (file)

BasicLemmas

FiniteDimensional

Lemmas

OrthonormalBasis

Submodule

DirectSumFromTo

End

InnerAut

InvariantSubmodule

IsProjPrime

IsReal

KroneckerToTensor

LinearMapOp

LmulRmul

MulPrimePrime

MyBimodule

MySpec

Nacgor

OfNorm

PiDirectSum

PiStarOrderedRing

PosMapIsReal

ToMatrixOfEquiv

Other (file)

Sonia

Preq (file)

Complex

Dite

Equiv

Finset

Ites

RCLikeLe

Set

StarAlgEquiv

QuantumGraph (file)

Basic

Degree

Example

Grad

Iso

Matrix

Nontracial

OfClassicalGraph

PiMat

PiMatFinTwo

QamA

QamAExample

ToProjections

RepTheory (file)

AutMat

Monlib

Monsky (file)

Appendix

BasicDefinitions

MainStatement

Miscellaneous

MonskyEven

RainbowTriangles

SegmentCounting

SegmentTriangle

SimplexBasic

Square

TriangleCorollary

Neukirch (file)

ExtensionOfDedekindDomains

HilbertRamificationTheory

OSforGFF (file)

Bochner (file)

FejerPD

Main

PositiveDefinite

Sazonov

Covariance (file)

Momentum

Parseval

Position

RealForm

GaussianField (file)

Nuclear (file)

DyninMityagin

NuclearSpace

NuclearTensorProduct

SchwartzNuclear (file)

Basis1D

HermiteFunctions

HermiteNuclear

HermiteTensorProduct

ParametricCalculus

SchwartzHermiteExpansion

SchwartzSlicing

General (file)

BesselFunction

FourierTransforms

FrobeniusPositivity

FunctionalAnalysis

GaussianRBF

HadamardExp

L2TimeIntegral

LaplaceIntegral

PositiveDefinite

QuantitativeDecay

SchurProduct

SchwartzTranslationDecay

KolmogorovExtension4 (file)

AuxLemmas

CompactSystem

KolmogorovExtension

RegularContent

Semiring

Measure (file)

Construct

GaussianFreeField

IsGaussian

Minlos

MinlosAnalytic

NuclearSpace

Minlos (file)

FinDimMarginals

Main

MeasurableModification

MinlosConcentration

NuclearSpace

PietschBridge

ProjectiveFamily

SazonovTightness

OS (file)

Axioms

Master

NonTrivial

OS0Analyticity

OS1Regularity

OS2Invariance

OS3CovarianceRP

OS3MixedRep

OS3MixedRepInfra

OS3ReflectionPositivity

OS4Clustering

OS4Ergodicity

OS4MGF

Schwinger (file)

Defs

GaussianMoments

TwoPoint

Spacetime (file)

Basic

ComplexTestFunction

Decomposition

DiscreteSymmetry

Euclidean

PositiveTimeTestFunction

ProdIntegrable

TimeTranslation

Tonelli

OrderPQ (file)

Basic

IsCyclic

Main

MonoidHom

MulZMod

PrimeOrder

SemidirectProduct

TorsionBy

PCFTheory (file)

Background (file)

Club

Cofinality

Ordinal

Topology

ClubGuessing

PLAcceleratedNesterovLean (file)

Convergence (file)

Bootstrap (file)

Main

Step1

Step2

Coercivity (file)

Core

Main

Step1

Step2

CurvAbsorb (file)

Algebraic

Assembly

LocalGeometry (file)

HessianBound

Main

SegmentEstimate

Step1

Step2

LyapunovContraction (file)

AuxVar

FlatCaseArithmetic

FlatCaseHelper

GenMain

Main

Step1

Step2

Step3

MotionError (file)

Main

StateContraction (file)

AuxVarRecursion

ConvergenceHelpers

GenLocalArgument

LocalArgument

MainTheoremInternal

NesterovConvergence

PhaseSchedule

RateArithmetic

Core (file)

Defs

EmbeddedManifold

NesterovScheme

NesterovSeqGen

MorseBott (file)

HessianPL (file)

Basics

Main

TubularProjection (file)

Defs

Derivative

IFT

Bridge

BridgeDefs

Defs

GradAlign

IFTProof

NormalHessianBound

PLImpliesMB

Submanifold

MainTheorem

PartialCombinatoryAlgebras (file)

Basic

CombinatoryAlgebra

FreeCombinatoryAlgebra

GraphModel

PartialCombinatoryAlgebra

Programming

PartialRegularity (file)

Extension

PebblingLean (file)

Basic

Concentration

Delivery

Examples

FiniteProbability

GraphIso

Hypercube

HypercubePath

HypercubeProduct

LowerBound

Paper

Product

UpperBound

UpperBoundDelivery

UpperBoundLoss

UpperBoundParameters

UpperBoundProbability

UpperBoundRecurrence

Weight

PentagonalNumberTheorem (file)

Complex

Generic

Old

Partition

PowerSeries

PhaseRetrieval (file)

Constant (file)

Internal

MissingMathlib

Poincare

AnnulusLocalEstimate

BlockDecomposition

Definitions

HighFreqBandEstimate

LaplaceFactorial

LeakageEstimate

LipschitzRho

Local

LocalCircleEstimate

LocalCore

LocalHelpers

MainTheorem

RotationalAveraging

SafeSquare

DimdPoly (file)

Internal

Hermite

Definitions

ImportedAnalyticInputs

MissingMathlib

Hermite1Dimd

BlockLocalization

Definitions

DegreeBookkeeping

ImportedAnalyticInputs

ProductAnnulusCircle

ProductBasisAndAnnuli

Hermitek

BasisLocalization

ImportedAnalyticInputs

ModulusRigidity

TrueLevelBasis

OrthogonalReduction

OrthogonalReduction

Auxiliary

CoefficientLimitRigidity

Definitions

ExactModulusRecovery

FiniteBaseAnnulusEstimate

FiniteBaseCircleEstimate

ImportedAnalyticInputs

OrthogonalCoercivity

PhaseStability

ProductAnnulusLocalization

TensorBasis

PointwiseBirkhoff (file)

Main

PolyaEnumerationTheorem (file)

Basic

Concrete

PermutationAuxiliary

ReductionToFin

StirlingFirstKindSum

Polylean (file)

Complexes (file)

Constructions

UniversalCover

Structures

Category

FreeGroupoid

Groupoid

Invertegory

Quiver

TwoComplex

GraphPaths

ConjInvLength (file)

Length

LengthBound

LengthNode

MemoLength

ProvedBound

WordTree

UnitConjecture (file)

Tactics (file)

AesopRuleSets

ReduceGoal

AddFreeGroup

Cocycle

EnumDecide

FreeModule

GardamGroup

GardamTheorem

GroupRing

MetabelianGroup

TorsionFree

Polymath

PolynomialMethodRestrictedSums (file)

ANRPolynomialMethod

CauchyDavenportTheorem

CompressedSizesRestrictedSum

DiasDaSilvaHamidoune

RestrictedSumDistinctSizes

VandermondeCoefficientFormula

Polytopes (file)

Cutspace

Halfspace

MainTheorem

Polar

Polytope

Pre

PumpingCfg (file)

ChomskyNormalForm

Basic

ContextFreeGrammarExtras

EmptyElimination

LengthRestriction

TerminalRestriction

Translation

UnitElimination

ParseTree

Pumping

ToMathlib

Utils

PythagoreanPolynomialParametrization (file)

Basic

Explanatory

IntegerValued

Main

Obstructions

Positive

SourceLemmas

QuasiBorelSpaces (file)

List (file)

Encoding

MeasureTheory (file)

Cases

Instances

List

Measure

Option

Pack

ProbabilityMeasure

Quantile

Randomization

Sigma

StandardBorelSpace

Sum

OmegaCompletePartialOrder (file)

Chain (file)

Const

Option

Sigma

Sum

Basic

Fix

Option

Sigma

Sum

Option (file)

Instances

Rose (file)

Encoding

RoseTree (file)

Basic

Defs

UnitInterval (file)

AssocProd

Basic

Chain

Cont

Defs

ENNReal

Finset

FlatReal

Functor

Hom

IsHomDiagonal

Lift

Multiset

Nat

OmegaHom

OmegaQuasiBorelSpace

Pi

PreProbabilityMeasure

ProbabilityMeasure

Prod

Prop

Quotient

SeparatesPoints

Sigma

Subtype

Sum

RamanujanNagell (file)

Basic

Helpers

RamanujanTauMissesPrimes (file)

Solution

Redhill (file)

Common

Conjectures

MaxAbs

PairwiseCoprime

PrimeChain

Quality

SubsumCondition

VWPair

General

Coprime

Defs

Main

Subsum

Odd

Defs

Main

Pell

Subsum

ToMathlib

NatAbs

NatSumProd

BB94

KonyaginPrelude

RiemannMappingTheorem (file)

Cindex

Defs

DerivInj

Etape2

HasSqrt

Hurwitz

Main

Montel

Spaces

ToMathlib

Uniform

RlTheoryInLean (file)

Analysis (file)

Normed (file)

Group (file)

Basic

Data (file)

Matrix (file)

Mul

PosDef

Stochastic

MeasureTheory (file)

Function (file)

ConditionalExpectation (file)

Basic

L1Space (file)

Integrable

MeasurableSpace (file)

Constructions

Measure (file)

GiryMonad

Prod

Order (file)

Filter (file)

Basic

Probability (file)

Kernel (file)

Composition (file)

MapComap

Basic

MarkovChain (file)

Finite (file)

Defs

Defs

Trajectory

StochasticApproximation (file)

DiscreteGronwall

Defs

RootSystem (file)

An

BCn

Rupert (file)

Equivalences

AffineRupertEquivRupertSet

RupertEquivRupertPrime

RupertEquivRupertSet

Util

Affine

Attr

Basic

Convex

Cube

FinCases

Icosahedron

MatrixSimps

Quaternion

Set

SnubCube

Square

Tetrahedron

TriakisTetrahedron

SardMoreira (file)

ToMathlib (file)

ContinuousLinearMap

PR31960

PR32186

PR32986

PR32993

PR33029

PR33114

Chart

ChartEstimates

ContDiff

ContDiffMoreiraHolder

ContinuousMultilinearMap

ImplicitFunction

LebesgueDensity

LinearAlgebra

LocalEstimates

MainTheorem

MeasureBallSemicontinuous

MeasureComap

MeasureNNReal

NormedSpace

OuterMeasureDeriv

Topology

UnifDoublingCover

Unused

UpperLowerSemicontinuous

WithRPowDist

SelbergSieve4 (file)

Applications (file)

BrunTitchmarsh

PrimeCountingUpperBound

ForMathlib (file)

Basic

ProdsAntidiagonal

Tactic (file)

AesopDiv

AesopInit

Multiplicativity

AuxResults

ForArithmeticFunction

MainResults

Selberg

SieveLemmas

UpperBoundSieve

SemicircleLaw (file)

SemicircleDistribution

Sensitivity (file)

Basic

Consequences

Defs

HuangBridge

Main

Multilinear

Parity

Subcube

SetTheory (file)

Basic

ElementaryEmbedding

KunenInconsistency

Omega

OrderTheory

Ordinals

Realize

SimpAttr

Shannon1948Formalization (file)

Entropy (file)

Approx

Converse

Core

Final

Gibbs

Joint

Properties

Rational

Uniform

SingularModuli (file)

QuadraticOrder

Prime (file)

Inert

PolyMod

QuotientIso

Ramified

Split

Basic

CanonicalForm

Discriminant

Norm

RootCounting

Verification

SpecialNumbers (file)

Euclidian

Eulerian

Sylvester

SumsThreeSquares (file)

MinkowskiConvex

SumThreeSquares

SyntheticEuclid4 (file)

Axioms

PermTactics

SyntheticEuclid4

Tactics

ThreeGap (file)

ChevallierCount

ChevallierGapBound

DeltaCost

EuclideanAngle

EuclideanDefect

EuclideanFiveDistanceSharp

EuclideanFiveDistanceSharpArith

EuclideanGrowth

EuclideanGrowthFive

EuclideanGrowthFour

EuclideanNN

EuclideanPacking

EuclideanRecords

FiveDistance

FiveDistanceHM

LinftyFiveDistanceSharpArith

LinftyThreeTorusNine

ModTwoGrowth

SimultaneousApprox

SimultaneousDirichlet

SupNormGrowth

TorusReduction

Turan3 (file)

Turans3rdProof

TwoColoringOneRound (file)

LowerBound (file)

Certificate

CorrAvgMatrix

Correlation

Defs

EdgePatterns

LocalRule

N1000000AvailFrom

N1000000BCompressionCompute

N1000000BCompressionComputeBase

N1000000BCompressionComputeS0

N1000000BCompressionComputeS0Int

N1000000BCompressionComputeS0IntBlock0

N1000000BCompressionComputeS0IntBlock1

N1000000BCompressionComputeS0IntBlock2

N1000000BCompressionComputeS0IntBlock3

N1000000BCompressionComputeS0IntBlock4

N1000000BCompressionComputeS0IntBlock5

N1000000BCompressionComputeS0IntBlock6

N1000000BCompressionComputeS0IntGoal

N1000000BCompressionComputeSi

N1000000BCompressionComputeSiInt

N1000000BCompressionComputeSiIntBlock0

N1000000BCompressionComputeSiIntBlock0Vars0to3

N1000000BCompressionComputeSiIntBlock0Vars12to15

N1000000BCompressionComputeSiIntBlock0Vars16to19

N1000000BCompressionComputeSiIntBlock0Vars20to22

N1000000BCompressionComputeSiIntBlock0Vars4to7

N1000000BCompressionComputeSiIntBlock0Vars8to11

N1000000BCompressionComputeSiIntBlock1

N1000000BCompressionComputeSiIntBlock1Vars0to3

N1000000BCompressionComputeSiIntBlock1Vars12to15

N1000000BCompressionComputeSiIntBlock1Vars16to19

N1000000BCompressionComputeSiIntBlock1Vars20to22

N1000000BCompressionComputeSiIntBlock1Vars4to7

N1000000BCompressionComputeSiIntBlock1Vars8to11

N1000000BCompressionComputeSiIntBlock2

N1000000BCompressionComputeSiIntBlock2Vars0to3

N1000000BCompressionComputeSiIntBlock2Vars12to15

N1000000BCompressionComputeSiIntBlock2Vars16to19

N1000000BCompressionComputeSiIntBlock2Vars20to22

N1000000BCompressionComputeSiIntBlock2Vars4to7

N1000000BCompressionComputeSiIntBlock2Vars8to11

N1000000BCompressionComputeSiIntBlock3

N1000000BCompressionComputeSiIntBlock3Vars0to3

N1000000BCompressionComputeSiIntBlock3Vars12to15

N1000000BCompressionComputeSiIntBlock3Vars16to19

N1000000BCompressionComputeSiIntBlock3Vars20to22

N1000000BCompressionComputeSiIntBlock3Vars4to7

N1000000BCompressionComputeSiIntBlock3Vars8to11

N1000000BCompressionComputeSiIntBlock4

N1000000BCompressionComputeSiIntBlock4Vars0to3

N1000000BCompressionComputeSiIntBlock4Vars12to15

N1000000BCompressionComputeSiIntBlock4Vars16to19

N1000000BCompressionComputeSiIntBlock4Vars20to22

N1000000BCompressionComputeSiIntBlock4Vars4to7

N1000000BCompressionComputeSiIntBlock4Vars8to11

N1000000BCompressionComputeSiIntBlock5

N1000000BCompressionComputeSiIntBlock5Vars0to3

N1000000BCompressionComputeSiIntBlock5Vars12to15

N1000000BCompressionComputeSiIntBlock5Vars16to19

N1000000BCompressionComputeSiIntBlock5Vars20to22

N1000000BCompressionComputeSiIntBlock5Vars4to7

N1000000BCompressionComputeSiIntBlock5Vars8to11

N1000000BCompressionComputeSiIntBlock6

N1000000BCompressionComputeSiIntBlock6Vars0to3

N1000000BCompressionComputeSiIntBlock6Vars12to15

N1000000BCompressionComputeSiIntBlock6Vars16to19

N1000000BCompressionComputeSiIntBlock6Vars20to22

N1000000BCompressionComputeSiIntBlock6Vars4to7

N1000000BCompressionComputeSiIntBlock6Vars8to11

N1000000BCompressionComputeSiIntGoal

N1000000BCompressionForB

N1000000Bound

N1000000CorrAvgMatrixDecompose

N1000000CorrAvgMatrixSymmDecompose

N1000000Data

N1000000Interface

N1000000IntersectionCounting

N1000000Main

N1000000MaskAtFacts

N1000000MaskComplete

N1000000MuLinear

N1000000MuWitness

N1000000Objective

N1000000OrbitCounting

N1000000OrbitalBasis

N1000000PairTransitivity

N1000000Relaxation

N1000000RelaxationPsdSoundness

N1000000StructureConstants

N1000000Transitivity

N1000000WeakDuality

N1000000WedderburnData

N1000000Witness

N1000000Z

N1000000ZData

N9

OverlapType

Sanity

UpperBound

UpperBound (file)

Recursive3Param (file)

Basic

Bound

ComputeP

Final

Regions

Value

API

Definitions

MainResults

Reduction

SimpleBounds

VirasoroProject (file)

ToMathlib (file)

Algebra (file)

Lie (file)

Abelian

Basic

LinearAlgebra (file)

Basis (file)

Defs

FinsumRepr

Finsupp (file)

Supported

Topology (file)

Algebra (file)

BigOperators (file)

FinProd

InfiniteSum (file)

Basic

Module (file)

LinearMap (file)

Defs

ConstMulAction

Order

CentralChargeCalc

CentralExtension

Commutator

CyclicTripleSum

FockSpace

FockSpaceSugawara

HeisenbergAlgebra

IndexTri

IsCentralExtension

LieAlgebraModuleUEA

LieAlgebraRepresentationOfBasis

LieCohomologySmallDegree

LieVerma

SectionSES

Sugawara

VermaModule

VirasoroAlgebra

VirasoroCocycle

VirasoroVerma

WittAlgebra

WittAlgebraCohomology

WhiteheadTheorem (file)

CWComplex

IProd

Def

Iso

Basic

Compressible

CWComplex

Defs

Disk

WeakEquiv

HEP

Cofibration

Cube

CubeJar

Retract

HomotopyGroup

ChangeBasePt

InducedMaps

RelHomotopyGroup

Algebra

Compression

Defs

LongExactSeq

Shapes

Cube

CubeBoundaryMap

Disk

DiskHomeoCube

Jar

MappingCylinder

Maps

Pushout

UnitInterval

Auxiliary

Basic

Defs

Exponential

ZFLean (file)

Basic

Booleans

Embeddings

Functions

Integers

Isomorphisms

IsomorphismsFunsToPowRel

IsomorphismsZFNatIso

Naturals

Rationals

Sum

Tactics

Zeta3Irrational (file)

Basic

Bound

Chebyshev

D

Equality

Integral

LegendrePoly

LinearForm

ZetaH123 (file)

H1

H2

H3

Lem41

ZhangYeungInequality (file)

PFR

ForMathlib

Entropy

Kernel

Basic

MutualInfo

Basic

Measure

FiniteRange

ConditionalProbability

Defs

ConditionalIndependence

Pair

Uniform

Mathlib

Analysis

SpecialFunctions

NegMulLog

Data

Set

Basic

Card

Insert

MeasureTheory

Constructions

Pi

Integral

Lebesgue

Basic

Countable

Measure

Dirac

Prod

Real

Probability

Independence

Kernel

IndepFun

Basic

Kernel

Composition

Comp

Disintegration

ConditionalProbability

IdentDistrib

UniformOn

Test (file)

CopyLemma

Delta

EntropyRegion

Theorem2

Theorem3

Theorem4

Theorem5

CopyLemma

Delta

EntropyRegion

Prelude

Theorem2

Theorem3

Theorem4

Theorem5

Basic

CramerWold

FundamentalInequality

UnconditionalSchauderBasis

LeanSearchClient (file)

Basic

LoogleSyntax

Syntax

Mathlib

Algebra

Algebra

Spectrum

Basic

Pi

Quasispectrum

Subalgebra

Basic

Directed

IsSimpleOrder

Lattice

Operations

Pointwise

Prod

Tower

Basic

Bilinear

Defs

Epi

Equiv

Hom

IsSimpleRing

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Rat

RestrictScalars

StrictPositivity

Tower

TransferInstance

Unitization

ZMod

Azumaya

Basic

Defs

Matrix

BigOperators

Finsupp

Basic

Fin

Group

Finset

Basic

Defs

Gaps

Indicator

Interval

Lemmas

Pi

Piecewise

Powerset

Preimage

Sigma

List

Basic

Defs

Lemmas

Multiset

Basic

Defs

GroupWithZero

Action

Finset

Ring

Finset

List

Multiset

Nat

Associated

Balance

Expect

Field

Fin

Finprod

Intervals

Module

NatAntidiagonal

Option

Pi

RingEquiv

WithTop

BrauerGroup

Defs

Category

AlgCat

Basic

FGModuleCat

Basic

Colimits

Limits

Grp

AB

Abelian

Adjunctions

Basic

Biproducts

Colimits

EpiMono

EquivalenceGroupAddGroup

FilteredColimits

ForgetCorepresentable

Injective

Kernels

Limits

Preadditive

Yoneda

ZModuleEquivalence

Zero

ModuleCat

Monoidal

Basic

Closed

Symmetric

Abelian

Adjunctions

Basic

Biproducts

ChangeOfRings

Colimits

EpiMono

Injective

Kernels

Limits

Products

Projective

Semi

MonCat

Basic

FilteredColimits

ForgetCorepresentable

Limits

Ring

Basic

Colimits

Constructions

Instances

Limits

Central

Basic

Defs

End

Matrix

TensorProduct

CharP

Algebra

Basic

CharAndCard

Defs

Frobenius

IntermediateField

Invertible

Lemmas

LinearMaps

Pi

Quotient

Reduced

Subring

Two

CharZero

AddMonoidHom

Defs

Infinite

Quotient

Colimit

DirectLimit

Finiteness

Module

TensorProduct

DirectSum

Algebra

Basic

Decomposition

Finsupp

Internal

Module

Ring

Divisibility

Basic

Hom

Prod

Units

EuclideanDomain

Basic

Defs

Field

Int

Exact

Basic

Field

Subfield

Basic

Defs

Basic

Defs

Equiv

GeomSum

IsField

NegOnePow

Opposite

Periodic

Rat

TransferInstance

ZMod

FiniteSupport

Basic

Defs

FreeAbelianGroup

Finsupp

FreeMonoid

Basic

UniqueProds

GCDMonoid

Basic

Finset

FinsetLemmas

IntegrallyClosed

Multiset

Nat

Group

Action

Pointwise

Set

Basic

Finite

Finset

Basic

Defs

End

Faithful

Hom

Opposite

Pi

Pretransitive

Prod

TransferInstance

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

Units

Pointwise

Finset

Basic

Scalar

Set

Basic

BigOperators

Card

Finite

Lattice

ListOfFn

Scalar

Small

Semiconj

Basic

Defs

Units

Subgroup

ZPowers

Basic

Lemmas

Actions

Basic

Defs

Even

Finite

Ker

Lattice

Map

MulOpposite

MulOppositeLemmas

Order

Pointwise

Submonoid

Basic

BigOperators

Defs

DistribMulAction

Finite

Membership

MulAction

MulOpposite

Operations

Pointwise

Units

Subsemigroup

Basic

Defs

Membership

MulOpposite

Operations

TypeTags

Basic

Finite

Hom

Pointwise

UniqueProds

Basic

Units

Basic

Defs

Equiv

Hom

Opposite

WithOne

Defs

Map

AddChar

Basic

Center

Commutator

Conj

ConjFinite

Defs

Embedding

End

Even

EvenFunction

Ext

Finsupp

Graph

Idempotent

Indicator

InjSurj

MinimalAxioms

ModEq

NatPowAssoc

Opposite

PUnit

Prod

Shrink

Support

Torsion

TransferInstance

ULift

GroupWithZero

Action

Pointwise

Set

Basic

Center

Defs

End

Hom

Opposite

Pi

Prod

TransferInstance

Units

Pointwise

Set

Basic

Submonoid

CancelMulZero

Instances

Pointwise

Primal

Units

Basic

Equiv

Fintype

Lemmas

Associated

Basic

Center

Commute

Conj

Defs

Divisibility

Equiv

Hom

Idempotent

Indicator

InjSurj

Invertible

Nat

NeZero

NonZeroDivisors

Opposite

Pi

Prod

Range

Regular

Semiconj

Subgroup

Torsion

ULift

WithZero

Homology

DerivedCategory

Ext

Basic

EnoughInjectives

ExactSequences

ExtClass

Basic

Fractions

FullyFaithful

HomologySequence

ShortExact

SingleTriangle

Embedding

AreComplementary

Basic

Boundary

CochainComplex

Extend

ExtendHomology

HomEquiv

IsSupported

Restriction

RestrictionHomology

TruncGE

TruncGEHomology

TruncLE

TruncLEHomology

HomotopyCategory (file)

Acyclic

DegreewiseSplit

HomComplex

HomComplexShift

HomologicalFunctor

MappingCocone

MappingCone

Pretriangulated

Shift

ShiftSequence

ShortExact

SingleFunctors

Triangulated

ShortComplex

Ab

Abelian

Basic

ConcreteCategory

Exact

ExactFunctor

HomologicalComplex

Homology

LeftHomology

Limits

ModuleCat

Preadditive

PreservesHomology

QuasiIso

Retract

RightHomology

ShortExact

SnakeLemma

Additive

CommSq

ComplexShape

ConcreteCategory

ExactSequence

HomologicalComplex

HomologicalComplexAbelian

HomologicalComplexBiprod

HomologicalComplexLimits

HomologySequence

HomologySequenceLemmas

Homotopy

HomotopyCofiber

ImageToKernel

Linear

Localization

Opposite

QuasiIso

Refinements

Single

SingleHomology

Lie

AdjointAction

Derivation

Derivation

Basic

Semisimple

Defs

Abelian

BaseChange

Basic

DirectSum

Ideal

IdealOperations

Matrix

Nilpotent

NonUnitalNonAssocAlgebra

Normalizer

OfAssociative

Quotient

Solvable

Subalgebra

Submodule

TensorProduct

UniversalEnveloping

Module

Congruence

Defs

Equiv

Basic

Defs

Opposite

LinearMap

Basic

Defs

DivisionRing

End

Prod

Rat

Star

LocalizedModule

AtPrime

Basic

Int

IsLocalization

Submodule

Submodule

Basic

Bilinear

Defs

EqLocus

Equiv

Finsupp

Invariant

IterateMapComap

Ker

Lattice

LinearMap

Map

Pointwise

Range

RestrictScalars

Torsion

Basic

Field

Free

Pi

Prod

Basic

BigOperators

Card

CharacterModule

DedekindDomain

Defs

End

FinitePresentation

Hom

Injective

MinimalAxioms

NatInt

Opposite

PID

PUnit

Pi

Prod

Projective

Rat

RingHom

Shrink

SpanRank

SpanRankOperations

TransferInstance

ULift

ZMod

MonoidAlgebra

Basic

Defs

Degree

Division

Lift

MapDomain

Module

NoZeroDivisors

Opposite

Support

MvPolynomial

Basic

Coeff

CommRing

Degrees

Derivation

Division

Equiv

Eval

Funext

Monad

NoZeroDivisors

PDeriv

Polynomial

Rename

Supported

Variables

NoZeroSMulDivisors

Basic

Defs

Notation (file)

Pi

Basic

Defs

Defs

FiniteSupport

Indicator

Lemmas

Prod

Support

Order

AbsoluteValue

Basic

Antidiag

Finsupp

Nat

Pi

Prod

Archimedean

Real

Basic

Hom

Basic

Defs

Hom

BigOperators

Group

Finset

List

LocallyFinite

Multiset

GroupWithZero

Finset

List

Multiset

Ring

Finset

List

Multiset

Expect

CauSeq

Basic

BigOperators

Completion

Field

Basic

Canonical

GeomSum

Pointwise

Power

Rat

Floor

Defs

Div

Ring

Semifield

Semiring

Group

Action (file)

Synonym

Pointwise

Bounds

CompleteLattice

Interval

Unbundled

Abs

Basic

Int

Abs

Basic

Cyclic

Defs

DenselyOrdered

Finset

Indicator

Int

Lattice

MinMax

Multiset

Nat

Opposite

OrderIso

PartialSups

PiLex

PosPart

Synonym

Units

GroupWithZero

Action

Synonym

Basic

Canonical

Defs

Finset

OrderIso

Range

Submonoid

Synonym

WithZero

Hom

Basic

Monoid

MonoidWithZero

Ring

TypeTags

Units

Interval

Finset

Basic

SuccPred

Set

Group

Instances

Monoid

Basic

Module

Basic

Defs

Field

Pointwise

PositiveLinearMap

Rat

Synonym

Monoid

Canonical

Basic

Defs

Unbundled

Basic

Defs

ExistsOfLE

MinMax

OrderDual

Pow

TypeTags

WithTop

Basic

Defs

LocallyFiniteOrder

NatCast

OrderDual

Prod

Submonoid

TypeTags

Units

WithTop

Nonneg

Basic

Field

Floor

Lattice

Module

Ring

Positive

Ring

Ring

Unbundled

Basic

Rat

Abs

Basic

Canonical

Cast

Defs

GeomSum

Idempotent

InjSurj

Int

Interval

IsNonarchimedean

Nat

Pow

Prod

Rat

Star

Synonym

WithTop

Star

Basic

Prod

Real

Sub

Unbundled

Basic

Basic

Defs

WithTop

SuccPred (file)

PartialSups

WithBot

WithTop

Untop0

AddGroupWithTop

AddTorsor

Algebra

Chebyshev

CompleteField

Disjointed

Invertible

IsBotOne

Kleene

Monovary

Pi

Rearrangement

Round

Sum

ToIntervalMod

ZeroLEOne

Pointwise

Stabilizer

Polynomial

Degree

Defs

Domain

Lemmas

Monomial

Operations

SmallDegree

Support

TrailingDegree

Units

Eval

Algebra

Coeff

Defs

Degree

SMul

Subring

Module

AEval

Basic

AlgebraMap

Basic

BigOperators

CancelLeads

Cardinal

Coeff

Derivation

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Monic

Monomial

OfFn

Reverse

RingDivision

Roots

Sequence

Smeval

SpecificDegree

Splits

Taylor

Prime

Defs

Lemmas

QuadraticAlgebra

Basic

Defs

NormDeterminant

Regular

Basic

Defs

Opposite

Pow

SMul

Ring

Action

Pointwise

Set

Basic

ConjAct

End

Field

Group

Invariant

Rat

Submonoid

Subobjects

Divisibility

Basic

Hom

Defs

InjSurj

Int

Defs

Field

Parity

Units

Submonoid

Basic

Pointwise

Subring

Basic

Defs

Pointwise

Units

Subsemiring

Basic

Defs

Pointwise

AddAut

Associated

Associator

Aut

Basic

Center

Centralizer

CharZero

Commute

CompTypeclasses

Defs

Equiv

Fin

GeomSum

GrindInstances

Idempotent

InjSurj

Invertible

IsFormallyReal

MinimalAxioms

Nat

NegOnePow

NonZeroDivisors

Opposite

PUnit

Parity

Periodic

Pi

Prod

Rat

Regular

Semiconj

Shrink

SumsOfSquares

Torsion

TransferInstance

ULift

Units

Squarefree

Basic

Star

Basic

BigOperators

Center

Module

MonoidHom

NonUnitalSubalgebra

Pi

Pointwise

Prod

Rat

SelfAdjoint

StarAlgHom

StarProjection

StarRingHom

Subalgebra

TensorProduct

Unitary

UnitaryStarAlgAut

Torsor

Basic

Defs

TrivSqZeroExt

Basic

FiveLemma

FreeAlgebra

GradedMonoid

IsPrimePow

LinearRecurrence

NeZero

Opposites

QuadraticDiscriminant

Quaternion

QuaternionBasis

Quotient

RingQuot

WithConv

AlgebraicTopology

FundamentalGroupoid

Basic

FundamentalGroup

InducedMaps

Product

RelativeCellComplex

AttachCells

Basic

SimplexCategory

Basic

Defs

DeltaZeroIter

Rev

Truncated

SimplicialObject

Basic

DeltaZeroIter

Homotopy

Op

SimplicialSet

Basic

CompStruct

CompStructTruncated

Degenerate

Dimension

Finite

Nerve

NerveNondegenerate

NonDegenerateSimplices

Op

Simplices

StdSimplex

Subcomplex

SubcomplexOp

AlternatingFaceMapComplex

CechNerve

ExtraDegeneracy

MooreComplex

Analysis

Analytic

Basic

CPolynomial

CPolynomialDef

ChangeOrigin

Composition

Constructions

ConvergenceRadius

Inverse

IsolatedZeros

IteratedFDeriv

Linear

OfScalars

Order

Polynomial

RadiusLiminf

Uniqueness

Within

Asymptotics

AsymptoticEquivalent

Defs

Lemmas

SpecificAsymptotics

TVS

Theta

BoxIntegral

Box

Basic

SubboxInduction

Partition

Additive

Basic

Filter

Measure

Split

SubboxInduction

Tagged

Basic

DivergenceTheorem

Integrability

CStarAlgebra

ContinuousFunctionalCalculus

Basic

Commute

Continuity

Instances

Isometric

NonUnital

Order

Pi

Restrict

Unique

Unital

Module

Defs

Basic

Classes

ContinuousLinearMap

ContinuousMap

Exponential

Fuglede

GelfandDuality

Matrix

Spectrum

Unitization

Calculus

BumpFunction

Basic

Convolution

FiniteDimension

InnerProduct

Normed

Conformal

NormedSpace

ContDiff

Basic

Bounds

CPolynomial

Comp

Convolution

Defs

Deriv

FTaylorSeries

FaaDiBruno

FiniteDimension

Operations

Polynomial

RCLike

RestrictScalars

WithLp

Deriv

Add

AffineMap

Basic

Comp

CompMul

Inv

Inverse

Linear

MeanValue

Mul

Polynomial

Pow

Prod

Shift

Slope

Star

Support

ZPow

FDeriv

Add

Affine

Analytic

Basic

Bilinear

Comp

CompCLM

Congr

Const

Defs

Equiv

Extend

Linear

Measurable

Mul

OfCompLeft

Pow

Prod

RestrictScalars

Star

Symmetric

WithLp

Gradient

Basic

ImplicitFunction

ProdDomain

InverseFunctionTheorem

Analytic

ApproximatesLinearOn

ContDiff

Deriv

FDeriv

IteratedDeriv

Defs

Lemmas

WithinZpow

LineDeriv

Basic

IntegrationByParts

LocalExtr

Basic

Rolle

TangentCone

Basic

Defs

DimOne

Prod

Real

DSlope

DiffContOnCl

FormalMultilinearSeries

Implicit

ImplicitContDiff

LagrangeMultipliers

LogDeriv

LogDerivUniformlyOn

MeanValue

Monotone

ParametricIntegral

ParametricIntervalIntegral

SmoothSeries

Taylor

UniformLimitsDeriv

Complex

Harmonic

Analytic

Polynomial

Basic

GaussLucas

UpperHalfPlane

Basic

Exp

FunctionsBoundedAtInfty

Manifold

Measure

MoebiusAction

Topology

AbsMax

Arg

Asymptotics

Basic

Cardinality

CauchyIntegral

Circle

Conformal

Convex

Exponential

ExponentialBounds

HalfPlane

HasPrimitives

IntegerCompl

IsIntegral

Isometry

Liouville

LocallyUniformLimit

Norm

OpenMapping

OperatorNorm

Order

Periodic

Positivity

ReImTopology

RealDeriv

RemovableSingularity

Schwarz

Spectrum

SummableUniformlyOn

TaylorSeries

Trigonometric

Convex

Cone

Extension

SpecificFunctions

Basic

Deriv

Pow

Basic

Between

Body

Combination

Contractible

Deriv

DoublyStochasticMatrix

EGauge

Exposed

Extreme

Function

Gauge

Hull

Independent

Integral

Intrinsic

Jensen

KreinMilman

Measure

Mul

NNReal

PartitionOfUnity

PathConnected

Piecewise

Segment

Side

Slope

Star

StdSimplex

Strict

StrictConvexSpace

Topology

TotallyBounded

Uniform

Distribution

SchwartzSpace

Basic

Deriv

Fourier

AEEqOfIntegralContDiff

DerivNotation

TemperateGrowth

TemperedDistribution

Fourier

AddCircle

BoundedContinuousFunctionChar

FourierTransform

FourierTransformDeriv

Inversion

LpSpace

Notation

PoissonSummation

RiemannLebesgueLemma

ZMod

InnerProductSpace

Harmonic

Basic

Constructions

Projection

Basic

FiniteDimensional

Minimal

Reflection

Submodule

Adjoint

Basic

Calculus

CanonicalTensor

Continuous

Convex

Defs

Dual

EuclideanDist

GramMatrix

GramSchmidtOrtho

Laplacian

LinearMap

MulOpposite

NormPow

Orientation

Orthogonal

Orthonormal

PiL2

Positive

ProdL2

Rayleigh

Semisimple

Spectrum

StarOrder

Subspace

Symmetric

TensorProduct

Trace

TwoDim

l2Space

LocallyConvex

AbsConvex

AbsConvexOpen

BalancedCoreHull

Barrelled

Basic

Bounded

HahnBanach

Polar

SeparatingDual

Separation

WeakDual

WithSeminorms

Matrix

Hermitian

HermitianFunctionalCalculus

Normed

Order

PosDef

Spectrum

Meromorphic

Basic

Divisor

IsolatedZeros

NormalForm

Order

Normed

Affine

AddTorsor

AddTorsorBases

Isometry

Algebra

Basic

Exponential

GelfandFormula

Spectrum

Unitization

UnitizationL1

Field

Basic

Instances

Lemmas

UnitBall

Group

AddCircle

AddTorsor

BallSphere

Basic

Bounded

Completion

Constructions

Continuity

Defs

FunctionSeries

Hom

Indicator

InfiniteSum

Int

Lemmas

NullSubmodule

Pointwise

Quotient

Rat

Real

Seminorm

Subgroup

Submodule

Tannery

Uniform

ZeroAtInfty

Lp

Matrix

MeasurableSpace

PiLp

ProdLp

SmoothApprox

WithLp

lpSpace

Module

Alternating

Basic

Ball

Homeomorph

Pointwise

RadialEquiv

Multilinear

Basic

Curry

RCLike

Basic

Extend

Real

Basic

Complemented

Completion

Connected

Convex

Dual

Extr

FiniteDimension

HahnBanach

MultipliableUniformlyOn

Normalize

Ray

RieszLemma

Shrink

Span

TransferInstance

WeakDual

Operator

Compact

Basic

FiniteDimension

FredholmAlternative

Asymptotics

Banach

BanachSteinhaus

Basic

Bilinear

BoundedLinearMaps

CompleteCodomain

Completeness

Conformal

ContinuousLinearMap

Extend

LinearIsometry

Mul

NNNorm

NormedSpace

Prod

Order

Lattice

Ring

Basic

Finite

InfiniteSum

Lemmas

Units

MulAction

ODE

Gronwall

Polynomial

Basic

RCLike

Basic

BoundedContinuous

Extend

Lemmas

Sqrt

TangentCone

Real

Pi

Bounds

Wallis

Cardinality

Spectrum

Sqrt

SpecialFunctions

Complex

Analytic

Arg

Circle

CircleAddChar

CircleMap

Log

LogBounds

LogDeriv

ContinuousFunctionalCalculus

PosPart

Basic

Rpow

Basic

Isometric

Abs

Gamma

Basic

Beta

BohrMollerup

Deligne

Deriv

Gaussian

FourierTransform

GaussianIntegral

PoissonSummation

Integrability

Basic

Integrals

Basic

Log

Base

Basic

Deriv

InvLog

Monotone

NegMulLog

Summable

Pow

Asymptotics

Complex

Continuity

Deriv

NNReal

Real

Trigonometric

Chebyshev

Basic

RootsExtrema

Angle

Arctan

ArctanDeriv

Basic

Bounds

Complex

ComplexDeriv

Cotangent

Deriv

DerivHyp

EulerSineProd

Inverse

Series

Sinc

Arcosh

Bernstein

Exp

ExpDeriv

Exponential

ImproperIntegrals

JapaneseBracket

MulExpNegMulSq

MulExpNegMulSqIntegral

NonIntegrable

Pochhammer

PolarCoord

PolynomialExp

Sigmoid

SmoothTransition

Sqrt

Stirling

SpecificLimits

ArithmeticGeometric

Basic

Normed

RCLike

VonNeumannAlgebra

Basic

BoundedVariation

Convolution

LConvolution

MeanInequalities

MeanInequalitiesPow

MellinTransform

Oscillation

PSeries

PSeriesComplex

Quaternion

Seminorm

SumIntegralComparisons

SumOverResidueClass

CategoryTheory

Abelian

DiagramLemmas

Four

GrothendieckAxioms

Basic

Colim

FunctorCategory

Sheaf

GrothendieckCategory

Basic

ColimCoyoneda

EnoughInjectives

HasExt

Monomorphisms

Subobject

Injective

Resolution

Projective

Resolution

Basic

CommSq

Exact

Ext

FunctorCategory

Images

LeftDerived

NonPreadditive

Opposite

Refinements

Subobject

Transfer

Action

Basic

Concrete

Limits

Monoidal

Adhesive

Basic

Adjunction

Additive

AdjointFunctorTheorems

Basic

Comma

FullyFaithful

Limits

Mates

Opposites

Parametrized

Reflective

Restrict

Unique

Whiskering

Bicategory

Functor

Lax

Oplax

Prelax

Pseudofunctor

Strict

Basic

Basic

Category

Cat (file)

AsSmall

Basic

GaloisConnection

Init

Pairwise

Pointed

Preorder

Quiv

ULift

Comma

Over

Basic

Pullback

Presheaf

Basic

StructuredArrow

Basic

Functor

Small

Arrow

Basic

CardinalArrow

LocallySmall

ComposableArrows

Basic

ConcreteCategory

Basic

Bundled

Elementwise

EpiMono

Forget

ReflectsIso

Discrete

Basic

StructuredArrow

EffectiveEpi

Basic

Endofunctor

Algebra

Filtered

Basic

Connected

Final

FinCategory

AsType

Basic

Functor

KanExtension

Adjunction

Basic

Pointwise

Preserves

ReflectsIso

Balanced

Basic

Basic

Category

Const

Currying

EpiMono

Flat

FullyFaithful

Hom

OfSequence

Trifunctor

TwoSquare

Generator

Basic

Presheaf

Sheaf

Groupoid (file)

Grpd

Basic

Idempotents

Basic

FunctorCategories

Karoubi

LiftingProperties

Adjunction

Basic

Limits

Limits

ConcreteCategory

Basic

Filtered

Constructions

BinaryProducts

EpiMono

Equalizers

EventuallyConstant

Filtered

FiniteProductsOfBinaryProducts

LimitsOfProductsAndEqualizers

Pullbacks

WeaklyInitial

Final (file)

Connected

FunctorCategory

Shapes

Terminal

Basic

EpiMono

Finite

Preserves

Creates

Finite

Pullbacks

Shapes

AbelianImages

BinaryProducts

Biproducts

Equalizers

Kernels

Preorder

Products

Pullbacks

Terminal

Zero

Basic

Bifunctor

Filtered

Finite

FunctorCategory

Limits

Opposites

Ulift

Shapes

NormalMono

Basic

Equalizers

Opposites

Equalizers

Filtered

Kernels

Products

Pullbacks

Preorder

Basic

Fin

HasIterationOfShape

PrincipalSeg

TransfiniteCompositionOfShape

WellOrderContinuous

Pullback

IsPullback

Basic

Defs

Assoc

Cospan

Equifibered

HasPullback

Iso

Mono

Pasting

PullbackCone

Square

BinaryBiproducts

BinaryProducts

Biproducts

ConcreteCategory

Countable

Diagonal

DisjointCoproduct

Equalizers

Equivalence

FiniteLimits

FiniteProducts

Grothendieck

Images

IsTerminal

KernelPair

Kernels

Multiequalizer

Products

RegularMono

SplitCoequalizer

SplitEqualizer

StrictInitial

StrongEpi

Terminal

WideEqualizers

WidePullbacks

ZeroMorphisms

ZeroObjects

Types

ColimitType

Colimits

Coproducts

Equalizers

Filtered

Images

Limits

Products

Pullbacks

Pushouts

Yoneda

Bicones

ColimitLimit

Comma

ConeCategory

Cones

Connected

Creates

EssentiallySmall

ExactFunctor

Filtered

FilteredColimitCommutesFiniteLimit

Fubini

FullSubcategory

HasLimits

IsConnected

IsLimit

Lattice

MonoCoprod

Opposites

Over

Preorder

Presentation

Presheaf

Sifted

Skeleton

Unit

VanKampen

Yoneda

Linear

Basic

FunctorCategory

LinearFunctor

Yoneda

Localization

CalculusOfFractions (file)

ComposableArrows

Fractions

Preadditive

Adjunction

Bousfield

Composition

Construction

Equivalence

HasLocalization

HomEquiv

LocalizerMorphism

Opposite

Predicate

SmallHom

SmallShiftedHom

Triangulated

Monad

Algebra

Basic

Products

Monoidal

Braided

Basic

Cartesian

Basic

FunctorCategory

Closed

Basic

Cartesian

Types

ExternalProduct

Basic

Limits

Preserves

Rigid

Basic

Braided

FunctorCategory

OfEquivalence

Types

Basic

Category

CoherenceLemmas

Discrete

End

Functor

FunctorCategory

Linear

NaturalTransformation

Opposite

Preadditive

Skeleton

Subcategory

Transport

MorphismProperty

Basic

Composition

Concrete

Factorization

IsInvertedBy

IsSmall

LiftingProperty

Limits

Retract

TransfiniteComposition

ObjectProperty

Basic

ClosedUnderIsomorphisms

ColimitsClosure

ColimitsOfShape

CompleteLattice

ContainsZero

Equivalence

FiniteProducts

FullSubcategory

LimitsClosure

LimitsOfShape

Local

Opposite

Retract

Shift

ShiftAdditive

Small

PathCategory

Basic

MorphismProperty

Pi

Basic

Preadditive

Injective

Basic

LiftingProperties

Preserves

Resolution

Projective

Basic

Preserves

Resolution

Yoneda

Basic

AdditiveFunctor

Basic

Biproducts

FunctorCategory

LeftExact

Opposite

Schur

Transfer

Presentable

IsCardinalFiltered

Products

Associator

Basic

Bifunctor

Unitor

Quotient (file)

Linear

Preadditive

Shift

Adjunction

Basic

CommShift

Induced

InducedShiftSequence

Localization

Opposite

Pullback

Quotient

ShiftSequence

ShiftedHom

ShiftedHomOpposite

SingleFunctors

Sites

DenseSubsite

Basic

InducedTopology

SheafEquiv

Hypercover

IsSheaf

One

Zero

SheafCohomology

Basic

Abelian

Canonical

Closed

CompatiblePlus

CompatibleSheafification

ConcreteSheafification

ConstantSheaf

Continuous

CoverLifting

CoverPreserving

Coverage

EpiMono

EqualizerSheafCondition

Equivalence

Grothendieck

InducedTopology

IsSheafFor

LeftExact

Limits

Localization

LocallyBijective

LocallyFullyFaithful

LocallyInjective

LocallySurjective

Plus

Precoverage

PrecoverageToGrothendieck

PreservesLocallyBijective

PreservesSheafification

Pretopology

Pullback

Sheaf

SheafOfTypes

Sheafification

Sieves

Spaces

Subsheaf

Whiskering

SmallObject

Iteration

Basic

ExtendToSucc

FunctorOfCocone

Nonempty

Basic

Construction

IsCardinalForSmallObjectArgument

TransfiniteCompositionLifting

TransfiniteIteration

WellOrderInductionData

Subfunctor

Basic

Image

OfSection

Sieves

Subobject

Basic

Comma

FactorThru

HasCardinalLT

Lattice

Limits

MonoOver

WellPowered

Triangulated

Opposite

Basic

Pretriangulated

Triangle

Basic

Functor

HomologicalFunctor

Pretriangulated

Rotate

Subcategory

TriangleShift

Triangulated

Yoneda

Types

Basic

Epimorphisms

Monomorphisms

WithTerminal

Basic

Cone

Balanced

CatCommSq

CofilteredSystem

CommSq

Conj

Countable

Elements

Elementwise

Endomorphism

EpiMono

EqToHom

Equivalence

EssentialImage

EssentiallySmall

Extensive

FintypeCat

GradedObject

Grothendieck

HomCongr

InducedCategory

IsConnected

Iso

IsomorphismClasses

NatIso

NatTrans

Opposites

PEmpty

PUnit

Retract

ShrinkYoneda

Simple

SingleObj

Skeletal

Square

Thin

Whiskering

Yoneda

Combinatorics

Digraph

Basic

Enumerative

Catalan

Basic

Partition

Basic

GenFun

Glaisher

Composition

DoubleCounting

InclusionExclusion

Hall

Basic

Finite

Matroid

Minor

Restrict

Rank

Cardinal

ENat

Finite

Basic

Circuit

Closure

Constructions

Dual

IndepAxioms

Init

Loop

Map

Quiver

Basic

Cast

Path

Prefunctor

Push

ReflQuiver

SingleObj

Symmetric

SetFamily

Compression

Down

Shatter

SimpleGraph

Coloring

Vertex

Connectivity

Connected

EdgeConnectivity

Finite

Subgraph

Walk

Basic

Chord

Counting

Decomp

Maps

Operations

Subwalks

Traversal

Acyclic

AdjMatrix

Basic

Bipartite

Clique

Copy

Dart

DegreeSum

DeleteEdges

Finite

Init

LapMatrix

Maps

Metric

Operations

Paths

Subgraph

Colex

Nullstellensatz

Computability

Primrec

Basic

List

TuringMachine

PostTuringMachine

StackTuringMachine

Tape

ContextFreeGrammar

DFA

Encoding

Halting

Language

MyhillNerode

Partrec

PartrecBasis

PartrecCode

RE

Reduce

StateTransition

Control

Monad

Basic

Cont

Writer

Traversable

Basic

Instances

Applicative

Basic

Bifunctor

Combinators

EquivFunctor

Functor

Lawful

ULift

ULiftable

Data

Bool

Basic

Set

Complex

Basic

BigOperators

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

Pow

EReal

Basic

Inv

Operations

Fin

Tuple

Basic

Embedding

NatAntidiagonal

Reflection

Sort

Basic

Embedding

Fin2

Rev

SuccPred

SuccPredOrder

VecNotation

Finite

Defs

Perm

Prod

Set

Sigma

Sum

Finset

Lattice

Basic

Fold

Lemmas

Prod

Union

Attach

Attr

Basic

BooleanAlgebra

Card

Dedup

Defs

Density

Disjoint

Empty

Erase

Filter

Fin

Finsupp

Fold

Image

Insert

Max

MulAntidiagonal

NAry

NatAntidiagonal

NatDivisors

NoncommProd

Option

Order

Pairwise

Pi

Piecewise

Powerset

Preimage

Prod

Range

SDiff

SMulAntidiagonal

Sigma

Slice

Sort

Sum

Sym

SymmDiff

Union

Update

Finsupp

MonomialOrder (file)

DegLex

Antidiagonal

Basic

Defs

Encodable

Ext

Fin

Fintype

Indicator

Interval

Lex

Multiset

Notation

Option

Order

PWO

Pointwise

SMul

SMulWithZero

Single

ToDFinsupp

Weight

WellFounded

Fintype

Basic

BigOperators

Card

CardEmbedding

Defs

EquivFin

Fin

Inv

Lattice

List

OfMap

Option

Order

Parity

Perm

Pi

Pigeonhole

Powerset

Prod

Quotient

Sets

Shrink

Sigma

Sort

Sum

Vector

WithTopBot

FunLike

Basic

Embedding

Equiv

Fintype

Group

IsApply

Module

Ring

Int

Cast

Basic

Defs

Field

Lemmas

Pi

Prod

Fib

Basic

Order

Basic

Lemmas

Units

Associated

Basic

CardIntervalMod

CharZero

ConditionallyCompleteOrder

DivMod

GCD

Init

Interval

LeastGreatest

Log

ModEq

NatAbs

NatPrime

Notation

Range

Sqrt

Star

SuccPred

WithZero

List

Perm

Basic

Lattice

Subperm

Basic

Chain

Count

Cycle

Dedup

Defs

Duplicate

Enum

FinRange

Flatten

Forall2

GetD

Induction

Infix

InsertIdx

Iterate

Lattice

Lex

MinMax

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

OffDiag

Pairwise

Permutation

Pi

Prime

ProdSigma

Range

Rotate

Sort

Sublists

Sym

TFAE

TakeDrop

ToFinsupp

Zip

Matrix

Basic

Basis

Block

ColumnRowPartitioned

Composition

Diagonal

Mul

PEquiv

Reflection

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

Order

NNReal

Basic

Defs

Star

Nat

Cast

Order

Basic

Field

Ring

Basic

Commute

Defs

Field

NeZero

Prod

WithTop

Choose

Basic

Bounds

Cast

Central

Dvd

Factorization

Multinomial

Sum

Vandermonde

Digits

Defs

Lemmas

Factorial

Basic

BigOperators

Cast

DoubleFactorial

SuperFactorial

Factorization

Basic

Defs

Induction

LCM

PrimePow

Fib

Basic

GCD

Basic

BigOperators

NthRoot

Defs

Order

Lemmas

Prime

Basic

Defs

Factorial

Infinite

Int

Nth

Pow

Basic

BinaryRec

BitIndices

Bits

Bitwise

ChineseRemainder

Count

Dist

Factors

Find

Init

Log

MaxPowDiv

ModEq

Multiplicity

Notation

Nth

PSub

Pairing

Periodic

PrimeFin

Set

Size

Sqrt

Squarefree

SuccPred

Totient

WithBot

Num

Basic

Bitwise

Lemmas

Option

Basic

Defs

NAry

Ordering

Basic

PFunctor

Univariate

Basic

M

PNat

Basic

Defs

Equiv

Interval

Notation

Prime

Pi

Interval

Prod

Basic

Lex

PProd

TProd

QPF

Univariate

Basic

Rat

Cast

CharZero

Defs

Lemmas

OfScientific

Order

BigOperators

Defs

Encodable

Floor

Init

Lemmas

Sqrt

Star

Real

Basic

ConjExponents

ENatENNReal

Pointwise

Sign

Star

Rel (file)

Cover

Separated

Set

Card (file)

Arithmetic

Finite

Basic

Lattice

Lemmas

Powerset

Range

Lattice (file)

Image

Pairwise

Basic

Lattice

List

Pointwise

Support

Basic

BoolIndicator

BooleanAlgebra

CoeSort

Constructions

Countable

Defs

Disjoint

Function

Functor

Image

Inclusion

Insert

List

MemPartition

Monotone

MulAntidiagonal

NAry

Notation

Operations

Order

Piecewise

Prod

Restrict

SMulAntidiagonal

Semiring

Sigma

Subset

Subsingleton

SymmDiff

UnionLift

SetLike

Basic

Fintype

Setoid

Partition (file)

Card

Basic

Sigma

Basic

Lex

Order

Sign

Basic

Defs

Stream

Defs

Init

String

Defs

Sum

Basic

Order

Sym

Sym2 (file)

Init

Basic

Card

Tree

Basic

Vector

Basic

Defs

W

Basic

Cardinal

ZMod

Aut

Basic

Coprime

Defs

IntUnitsPower

QuotientGroup

QuotientRing

Units

ValMinAbs

Bracket

Bundle

FinEnum

Ineq

Opposite

PEquiv

PFun

Part

Quot

SProd

Subtype

ULift

Vector3

Dynamics

BirkhoffSum

Average

Basic

QuasiMeasurePreserving

Ergodic

Action

Basic

Regular

Ergodic

MeasurePreserving

FixedPoints

Basic

Defs

Topology

PeriodicPts

Defs

Lemmas

Minimal

FieldTheory

Finite

Basic

GaloisField

Trace

Galois

Abelian

Basic

GaloisClosure

Infinite

Notation

IntermediateField

Adjoin

Algebra

Basic

Defs

Algebraic

Basic

IsAlgClosed

AlgebraicClosure

Basic

Spectrum

Minpoly

Basic

Field

Finite

IsIntegrallyClosed

MinpolyDiv

Normal

Basic

Closure

Defs

PurelyInseparable

Basic

RatFunc

AsPolynomial

Basic

Defs

SplittingField

Construction

IsSplittingField

AlgebraicClosure

Extension

Finiteness

Fixed

IsSepClosed

JacobsonNoether

KrullTopology

KummerPolynomial

Perfect

PerfectClosure

PolynomialGaloisGroup

PrimitiveElement

Separable

SeparableClosure

SeparableDegree

Tower

Geometry

Convex

Cone

Basic

Euclidean

Angle

Oriented

Affine

Basic

Rotation

Unoriented

Affine

Basic

TriangleInequality

Projection

Triangle

Manifold

Algebra

LieGroup

Monoid

SMul

Structures

ContMDiff

Atlas

Basic

Constructions

Defs

NormedSpace

IsManifold

Basic

ExtChartAt

MFDeriv

Atlas

Basic

Defs

FDeriv

SpecificFunctions

UniqueDifferential

VectorBundle

Basic

ContMDiffSection

FiberwiseLinear

Tangent

BumpFunction

ChartedSpace

ContMDiffMap

Diffeomorph

HasGroupoid

Immersion

LocalInvariantProperties

LocalSourceTargetProperty

Notation

PartitionOfUnity

SmoothApprox

SmoothEmbedding

StructureGroupoid

GroupTheory

Abelianization

Defs

Finite

Commutator

Basic

Congruence

Basic

BigOperators

Defs

Hom

Opposite

Coprod

Basic

Coset

Basic

Card

Defs

Coxeter

Basic

Inversion

Length

Matrix

FiniteAbelian

Basic

Duality

FreeGroup

Basic

GroupAction

DomAct

Basic

SubMulAction (file)

OfFixingSubgroup

OfStabilizer

Pointwise

Basic

Blocks

CardCommute

ConjAct

Defs

Embedding

FixedPoints

FixingSubgroup

Hom

IterateAct

MultipleTransitivity

Pointwise

Primitive

Quotient

Ring

Transitive

MonoidLocalization

Away

Basic

Cardinality

Maps

MonoidWithZero

OreLocalization

Basic

Cardinality

OreSet

Perm

Cycle

Basic

Factors

Type

Basic

Closure

ConjAct

Fin

Finite

List

Option

Sign

Support

ViaEmbedding

QuotientGroup

Basic

Defs

Finite

ModEq

SpecificGroups

Cyclic (file)

Basic

Alternating

Dihedral

KleinFour

Subgroup

Center

Centralizer

Simple

Submonoid

Center

Centralizer

Subsemigroup

Center

Centralizer

Archimedean

ArchimedeanDensely

ClassEquation

Commensurable

CommutingProbability

Complement

DedekindFinite

Divisible

DoubleCoset

EckmannHilton

Exponent

Finiteness

FreeAbelianGroup

Index

IndexNormal

NoncommPiCoprod

OrderOfElement

PGroup

PresentedGroup

Rank

SemidirectProduct

Solvable

Sylow

Torsion

Lean

Elab

Tactic

Meta

InfoTree

Term

Expr

Basic

ExtraRecognizers

Rat

MessageData

Trace

Meta (file)

RefinedDiscrTree (file)

Basic

Encode

Initialize

Lookup

Tactic

Rewrite

Basic

CongrTheorems

KAbstractPositions

Simp

PrettyPrinter

Delaborator

ContextInfo

Environment

GoalsLocation

Linter

Name

LinearAlgebra

AffineSpace

AffineSubspace

Basic

Defs

Simplex

Basic

Centroid

AffineEquiv

AffineMap

Basis

Centroid

Combination

Defs

FiniteDimensional

Independent

Midpoint

Ordered

Pointwise

Restrict

Slope

Alternating

Basic

Curry

Basis

Basic

Bilinear

Cardinality

Defs

Fin

MulOpposite

Prod

SMul

Submodule

VectorSpace

BilinearForm

Basic

DualLattice

Hom

Properties

Charpoly

BaseChange

Basic

ToMatrix

Complex

Determinant

FiniteDimensional

Module

Orientation

Dimension

Basic

Constructions

DivisionRing

ErdosKaplansky

Finite

Finrank

Free

FreeAndStrongRankCondition

LinearMap

Localization

OrzechProperty

RankNullity

StrongRankCondition

Subsingleton

DirectSum

Finite

Finsupp

TensorProduct

Dual

BaseChange

Basis

Defs

Lemmas

Eigenspace

Basic

Charpoly

ContinuousLinearMap

Matrix

Minpoly

FiniteDimensional

Basic

Defs

Lemmas

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

CardQuotient

Matrix

Quotient

Basic

Determinant

PID

StrongRankCondition

GeneralLinearGroup

AlgEquiv

Basic

LinearIndependent

Basic

Defs

Lemmas

Matrix

Charpoly

Basic

Coeff

Disc

Eigs

LinearMap

Minpoly

Determinant

Basic

GeneralLinearGroup

Basic

Defs

FinTwo

Projective

Action

Adjugate

BaseChange

Basis

BilinearForm

Block

ConjTranspose

Defs

Diagonal

DotProduct

Dual

FiniteDimensional

FixedDetMatrices

Hadamard

Hermitian

Ideal

Integer

InvariantBasisNumber

Invertible

IsDiag

Kronecker

MvPolynomial

Nondegenerate

NonsingularInverse

Notation

Orthogonal

Permutation

Polynomial

PosDef

ProjectiveSpecialLinearGroup

Rank

Reindex

RowCol

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

StdBasis

Stochastic

Swap

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

Vec

ZPow

Multilinear

Basic

Basis

Curry

DFinsupp

Finsupp

PerfectPairing

Basic

Restrict

Projectivization

Action

Basic

Cardinality

Independence

QuadraticForm

Basic

Quotient

Basic

Card

Defs

Pi

RootSystem

Defs

IsValuedIn

OfBilinear

Reduced

SModEq

Basic

Pointwise

SesquilinearForm

Basic

Span

Basic

Defs

TensorProduct

TensorAlgebra

Basic

TensorProduct

Associator

Basic

Basis

Defs

DirectLimit

Finiteness

Map

Matrix

Opposite

Pi

Prod

Quotient

RightExactness

Submodule

Tower

Vanishing

Transvection

Basic

AnnihilatingPolynomial

BilinearMap

Center

Coevaluation

Contraction

CrossProduct

DFinsupp

Determinant

FiniteSpan

FixedSubmodule

InvariantBasisNumber

Isomorphisms

Lagrange

LinearDisjoint

LinearPMap

Orientation

Pi

Prod

Projection

Ray

Reflection

Semisimple

SpecialLinearGroup

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

CompTypeclasses

Conjugate

Defs

DependsOn

Iterate

ULift

Godel

GodelBetaFunction

IsEmpty

Basic

Defs

Nontrivial

Basic

Defs

Small

Basic

Defs

List

Set

Basic

Denumerable

ExistsUnique

Lemmas

Nonempty

OpClass

Pairwise

Relation

Relator

Unique

UnivLE

MeasureTheory

Constructions

BorelSpace

Basic

Complex

ContinuousLinearMap

Metric

Metrizable

Order

Real

WithTop

Polish

Basic

EmbeddingReal

StronglyMeasurable

ClosedCompactCylinders

Cylinders

HaarToSphere

Pi

Projective

ProjectiveFamilyContent

UnitInterval

Covering

Besicovitch

BesicovitchVectorSpace

DensityTheorem

Differentiation

LiminfLimsup

OneDim

Vitali

VitaliFamily

Function

AEEqFun (file)

DomAct

ConditionalExpectation

AEMeasurable

Basic

CondexpL1

CondexpL2

Indicator

PullOut

Real

Unique

L1Space

AEEqFun

HasFiniteIntegral

Integrable

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

Defs

Indicator

LpNorm

Monotonicity

Prod

SMul

TriangleInequality

Trim

LpSpace

DomAct

Basic

Continuous

Basic

Complete

CompleteOfCompleteLp

ContinuousCompMeasurePreserving

ContinuousFunctions

Indicator

InfiniteSum

SpecialFunctions

Basic

Inner

RCLike

Sinc

StronglyMeasurable

AEStronglyMeasurable

Basic

ENNReal

Inner

Lemmas

Lp

AEEqOfIntegral

AEEqOfLIntegral

AEMeasurableOrder

AEMeasurableSequence

AbsolutelyContinuous

ContinuousMapDense

ConvergenceInMeasure

Egorov

EssSup

FactorsThrough

Floor

Holder

Jacobian

JacobianOneDim

L2Space

LocallyIntegrable

LpOrder

SimpleFunc

SimpleFuncDense

SimpleFuncDenseLp

UniformIntegrable

Group

AEStabilizer

Action

Arithmetic

Convolution

Defs

FundamentalDomain

GeometryOfNumbers

Integral

IntegralConvolution

LIntegral

MeasurableEquiv

Measure

Pointwise

Prod

Integral

Bochner

Basic

ContinuousLinearMap

FundThmCalculus

L1

Set

SumMeasure

VitaliCaratheodory

IntervalIntegral

AbsolutelyContinuousFun

Basic

DerivIntegrable

FundThmCalculus

IntegrationByParts

LebesgueDifferentiationThm

Periodic

Slope

Lebesgue

Add

Basic

Countable

DominatedConvergence

Map

Markov

Norm

Sub

RieszMarkovKakutani

Basic

Real

Asymptotics

Average

BoundedContinuousFunction

CircleAverage

CircleIntegral

CompactlySupported

DivergenceTheorem

DominatedConvergence

ExpDecay

FinMeasAdditive

Gamma

IntegrableOn

IntegralEqImproper

IntervalAverage

Layercake

Marginal

MeanInequalities

PeakFunction

Pi

Prod

Regular

SetToL1

MeasurableSpace

Basic

Constructions

CountablyGenerated

Defs

Embedding

EventuallyMeasurable

Instances

Invariants

MeasurablyGenerated

Pi

PreorderRestrict

Prod

Measure

CharacteristicFunction

Basic

Decomposition

Exhaustion

Hahn

Lebesgue

RadonNikodym

Haar

Basic

InnerProductSpace

NormedSpace

OfBasis

Quotient

Unique

Lebesgue

Basic

Complex

EqHaar

Integral

VolumeOfBalls

Typeclasses

Finite

NoAtoms

Probability

SFinite

AEDisjoint

AEMeasurable

AbsolutelyContinuous

AddContent

Comap

Complex

Content

ContinuousPreimage

Count

Dirac

DiracProba

Doubling

EverywherePos

FiniteMeasure

FiniteMeasureExt

FiniteMeasureProd

GiryMonad

HasOuterApproxClosed

Hausdorff

IntegralCharFun

LevyProkhorovMetric

Map

MeasureSpace

MeasureSpaceDef

MutuallySingular

NullMeasurable

OpenPos

Portmanteau

ProbabilityMeasure

Prod

Prokhorov

QuasiMeasurePreserving

Real

Regular

RegularityCompacts

Restrict

Stieltjes

Sub

Support

Tight

TightNormed

Tilted

Trim

WithDensity

Order

Group

Lattice

Lattice

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfAddContent

OfFunction

Operations

SpecificCodomains

Pi

VectorMeasure

Decomposition

Hahn

Jordan

Lebesgue

RadonNikodym

Basic

WithDensity

PiSystem

SetAlgebra

SetSemiring

Topology

ModelTheory

Basic

Bundled

Complexity

Definability

DirectLimit

ElementaryMaps

ElementarySubstructures

Encoding

Equivalence

FinitelyGenerated

Fraisse

LanguageMap

Order

PartialEquiv

Quotients

Satisfiability

Semantics

Skolem

Substructures

Syntax

Ultraproducts

NumberTheory

ArithmeticFunction

Defs

Misc

Moebius

VonMangoldt

Zeta

Cyclotomic

Basic

PrimitiveRoots

DiophantineApproximation

Basic

DirichletCharacter

Basic

Bounds

GaussSum

Orthogonality

EulerProduct

Basic

DirichletLSeries

ExpLog

Harmonic

Bounds

Defs

EulerMascheroni

GammaDeriv

ZetaAsymp

LSeries

AbstractFuncEq

Basic

Convergence

Convolution

Deriv

Dirichlet

DirichletContinuation

HurwitzZeta

HurwitzZetaEven

HurwitzZetaOdd

HurwitzZetaValues

Linearity

MellinEqDirichlet

Nonvanishing

Positivity

PrimesInAP

RiemannZeta

ZMod

LegendreSymbol

QuadraticChar

Basic

GaussSum

AddCharacter

Basic

JacobiSymbol

QuadraticReciprocity

ZModChar

ModularForms

EisensteinSeries

E2

Defs

Summable

Transform

Basic

Defs

IsBoundedAtImInfty

MDifferentiable

QExpansion

Summable

UniformConvergence

JacobiTheta

Bounds

TwoVariable

LevelOne

Basic

ArithmeticSubgroups

Basic

BoundedAtCusp

Bounds

CongruenceSubgroups

Cusps

DedekindEta

Identities

Petersson

QExpansion

SlashActions

SlashInvariantForms

MulChar

Basic

Duality

Lemmas

NumberField

Basic

Norm

Padics

PadicVal

Basic

Defs

PadicNorm

PadicNumbers

RamificationInertia

Basic

Inertia

Ramification

Real

GoldenRatio

Irrational

Zsqrtd

Basic

GaussianInt

QuadraticReciprocity

AbelSummation

Bernoulli

BernoulliPolynomials

Bertrand

Chebyshev

Divisors

FrobeniusNumber

GaussSum

KummerDedekind

Modular

Multiplicity

Niven

PrimeCounting

Primorial

PythagoreanTriples

SmoothNumbers

SumFourSquares

SumPrimeReciprocals

SumTwoSquares

TsumDivisorsAntidiagonal

ZetaValues

Order

Atoms (file)

Finite

BooleanAlgebra

Basic

Defs

Set

BoundedOrder

Basic

Lattice

Monotone

Bounds

Basic

Defs

Image

OrderIso

Category

FinPartOrd

Lat

LinOrd

NonemptyFinLinOrd

PartOrd

Preord

CompactlyGenerated

Basic

Intervals

CompleteLattice

Basic

Chain

Defs

Finset

Group

Lemmas

SetLike

ConditionallyCompleteLattice

Basic

Defs

Finset

Group

Indexed

ConditionallyCompletePartialOrder

Basic

Defs

Indexed

Defs

LinearOrder

PartialOrder

Unbundled

Filter

AtTopBot

Archimedean

Basic

BigOperators

CompleteLattice

CountablyGenerated

Defs

Disjoint

Field

Finite

Finset

Floor

Group

Interval

Map

ModEq

Monoid

Prod

Ring

Tendsto

Bases

Basic

Finite

Germ

Basic

OrderedMonoid

Ultrafilter

Basic

Defs

Basic

Cofinite

CountableInter

CountableSeparatingOn

CountablyGenerated

Curry

Defs

ENNReal

EventuallyConst

Extr

Finite

IndicatorFunction

Interval

IsBounded

Ker

Lift

Map

NAry

Pi

Pointwise

Prod

Ring

SmallSets

Subsingleton

Tendsto

TendstoCofinite

ZeroAndBoundedAtFilter

Fin

Basic

Finset

SuccAboveOrderIso

Tuple

GaloisConnection

Basic

Defs

Heyting

Basic

Boundary

Hom

Regular

Hom

Basic

Bounded

BoundedLattice

CompleteLattice

Lattice

Lex

Order

Set

WithTopBot

Interval

Finset

Basic

Box

Defs

DenselyOrdered

Fin

Gaps

Nat

SuccPred

Set

Basic

Defs

Disjoint

Fin

Final

Image

Infinite

InitialSeg

IsoIoo

Limit

LinearOrder

Monotone

OrdConnected

OrdConnectedComponent

OrderEmbedding

OrderIso

Pi

ProjIcc

SuccOrder

SuccPred

Union

UnorderedInterval

WithBotTop

Basic

Multiset

Lattice (file)

Nat

Monotone

Basic

Defs

Extension

Monovary

Odd

Union

Partition

Finpartition

Preorder

Chain

Finite

Finsupp

RelIso

Basic

Set

SuccPred

Archimedean

Basic

CompleteLinearOrder

InitialSeg

IntervalSucc

Limit

LinearLocallyFinite

Relation

WithBot

UpperLower

Basic

Closure

CompleteLattice

Fibration

Principal

Antichain

Antisymmetrization

Basic

BooleanSubalgebra

BourbakiWitt

Circular

Closure

Cofinal

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

CompletePartialOrder

CompleteSublattice

Copy

CountableDenseLinearOrder

Cover

DirSupClosed

Directed

DirectedInverseSystem

Disjoint

Disjointed

FixedPoints

GameAdd

Grade

Ideal

InitialSeg

IsNormal

Iterate

JordanHolder

KonigLemma

KrullDimension

LatticeIntervals

Lex

LiminfLimsup

Max

MinMax

Minimal

ModularLattice

Nat

Notation

OmegaCompletePartialOrder

OrdContinuous

OrderDual

OrderIsoNat

Part

PartialSups

PiLex

PropInstances

RelClasses

RelSeries

Restriction

ScottContinuity

SetAccumulate

SetDissipate

SetIsMax

SetNotation

Shrink

Sublattice

SupClosed

SupIndep

SymmDiff

TransfiniteIteration

TypeTags

ULift

WellFounded

WellFoundedSet

WellQuasiOrder

WithBot

WithBotTop

Zorn

ZornAtoms

Probability

Distributions

Gaussian

Basic

Fernique

Real

Bernoulli

Fernique

Independence

Kernel

Indep

IndepFun

Basic

Integrable

Integration

Kernel

Composition

Comp

CompMap

CompNotation

CompProd

IntegralCompProd

KernelLemmas

Lemmas

MapComap

MeasureComp

MeasureCompProd

ParallelComp

Prod

Disintegration

Basic

CDFToKernel

CondCDF

Density

Integral

MeasurableStieltjes

StandardBorel

Unique

IonescuTulcea

Maps

PartialTraj

Traj

Basic

CondDistrib

Condexp

Defs

Integral

MeasurableIntegral

MeasurableLIntegral

SetIntegral

Martingale

Basic

Convergence

Upcrossing

Moments

Basic

ComplexMGF

Covariance

IntegrableExpMul

MGFAnalytic

SubGaussian

Tilted

Variance

ProbabilityMassFunction

Basic

Constructions

Monad

Process

Adapted

Filtration

HittingTime

PartitionFiltration

Predictable

Stopping

CDF

ConditionalProbability

Density

HasLaw

IdentDistrib

Notation

ProductMeasure

UniformOn

RepresentationTheory

Homological

GroupCohomology

Basic

LowDegree

Resolution

Rep

Basic

Iso

Res

Action

Basic

Equiv

FDRep

Intertwining

Invariants

Subrepresentation

RingTheory

AdicCompletion

Algebra

AsTensorProduct

Basic

Exactness

Functoriality

Noetherian

RingHom

Adjoin

Polynomial

Basic

Basic

Dimension

FG

FGBaseChange

Field

PowerBasis

Singleton

Tower

Algebraic

Basic

Defs

Integral

MvPolynomial

AlgebraicIndependent

Adjoin

AlgebraicClosure

Basic

Defs

TranscendenceBasis

Transcendental

Artinian

Defs

Instances

Module

Ring

Bialgebra

Basic

Convolution

Equiv

Hom

TensorProduct

ClassGroup

Basic

Coalgebra

Basic

CoassocSimps

Convolution

Equiv

Hom

TensorProduct

Congruence

Basic

BigOperators

Defs

Opposite

Coprime

Basic

Ideal

Lemmas

DedekindDomain

Ideal

Basic

Lemmas

AdicValuation

Basic

Dvr

Factorization

IntegralClosure

Derivation

Basic

DiscreteValuationRing

Basic

TFAE

Finiteness

Basic

Bilinear

Cardinality

Defs

Finsupp

Ideal

Lattice

Nakayama

Prod

Projective

Quotient

Small

Subalgebra

Flat

FaithfullyFlat

Algebra

Basic

Basic

EquationalCriterion

Localization

Stability

Tensor

TorsionFree

FractionalIdeal

Basic

Inverse

Operations

GradedAlgebra

Basic

HahnSeries

Addition

Basic

Multiplication

PowerSeries

Summable

HopfAlgebra

Basic

Convolution

Ideal

AssociatedPrime

Basic

Finiteness

Localization

MinimalPrime

Basic

Colon

Localization

Noetherian

Norm

AbsNorm

Quotient

Basic

ChineseRemainder

Defs

Nilpotent

Noetherian

Operations

PowTransition

Basic

Basis

BigOperators

Colon

Cotangent

Defs

GoingDown

GoingUp

Height

IsPrimary

IsPrincipal

KrullsHeightTheorem

Lattice

Maps

Maximal

NatInt

Nonunits

Oka

Operations

Over

Pointwise

Prime

Prod

Span

Int

Basic

IntegralClosure

Algebra

Basic

Defs

IsIntegral

Basic

Defs

IsIntegralClosure

Basic

Defs

IntegrallyClosed

Jacobson

Ideal

Polynomial

Radical

Ring

Semiprimary

KrullDimension

Basic

Field

Module

NonZeroDivisors

PID

Regular

Zero

LocalProperties

Basic

Exactness

IntegrallyClosed

Submodule

LocalRing

MaximalIdeal

Basic

Defs

ResidueField

Basic

Defs

Ideal

RingHom

Basic

Basic

Defs

Module

Localization

AtPrime

Basic

Away

Basic

Algebra

AsSubring

BaseChange

Basic

Cardinality

Defs

Finiteness

FractionRing

Ideal

Integer

Integral

LocalizationLocalization

Module

NormTrace

NumDen

Submodule

Morita

Basic

MvPolynomial

MonomialOrder (file)

DegLex

Symmetric

Defs

FundamentalTheorem

Basic

Groebner

Homogeneous

Tower

WeightedHomogeneous

MvPowerSeries

Basic

Evaluation

Inverse

LexOrder

LinearTopology

NoZeroDivisors

Order

PiTopology

Rename

Substitution

Trunc

Nilpotent

Basic

Defs

Exp

Lemmas

Noetherian

Basic

Defs

Nilpotent

OfPrime

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Basic

Defs

Transitivity

OreLocalization

Basic

Cardinality

NonZeroDivisors

OreSet

Ring

Polynomial

Cyclotomic

Basic

Eval

Expand

Roots

Eisenstein

Basic

Criterion

Hermite

Basic

Gaussian

Resultant

Basic

Basic

Bernstein

Chebyshev

Content

DegreeLT

GaussLemma

HilbertPoly

Ideal

IntegralNormalization

Nilpotent

Pochhammer

Quotient

RationalRoot

ScaleRoots

SeparableDegree

Subring

Tower

UniqueFactorization

Vieta

PowerSeries

Basic

Derivative

Evaluation

Exp

Ideal

Inverse

Log

NoZeroDivisors

Order

PiTopology

Substitution

Trunc

WellKnown

Radical

Basic

NatInt

Regular

IsSMulRegular

RegularSequence

RegularLocalRing

Defs

RootsOfUnity

AlgebraicallyClosed

Basic

Complex

EnoughRootsOfUnity

Minpoly

PrimitiveRoots

SimpleModule

Basic

Rank

SimpleRing

Basic

Defs

Field

Matrix

Principal

Spectrum

Maximal

Basic

Defs

Localization

Prime

Basic

Defs

LTSeries

Module

Noetherian

RingHom

Topology

TensorProduct

Basic

Finite

Free

IsBaseChangeFree

IsBaseChangeHom

IsBaseChangePi

Maps

MvPolynomial

Quotient

Trace

Basic

Defs

TwoSidedIdeal

Basic

BigOperators

Kernel

Lattice

Operations

UniqueFactorizationDomain

Basic

ClassGroup

Defs

FactorSet

Finite

Finsupp

GCDMonoid

Ideal

Kaplansky

Multiplicative

Multiplicity

Nat

NormalizedFactors

Valuation

Discrete

Basic

ValuativeRel

Basic

Basic

ExtendToLocalization

Extension

Integers

IsTrivialOn

PrimeMultiplicity

ValuationRing

ValuationSubring

ZMod (file)

UnitsCyclic

AdjoinRoot

AlgebraTower

Bezout

Binomial

ChainOfDivisors

Complex

Conductor

Discriminant

EssentialFiniteness

EuclideanDomain

Filtration

FiniteLength

FinitePresentation

FiniteType

Henselian

HopkinsLevitzki

IntegralDomain

IsAdjoinRoot

IsPrimary

IsTensorProduct

LaurentSeries

Length

LittleWedderburn

MatrixAlgebra

MatrixPolynomialAlgebra

Multiplicity

Nakayama

OrzechProperty

PicardGroup

PolynomialAlgebra

PowerBasis

PrincipalIdealDomain

PrincipalIdealDomainOfPrime

QuotSMulTop

ReesAlgebra

RingHomProperties

Support

SurjectiveOnStalks

SetTheory

Cardinal

Cofinality

Basic

Enum

Ordinal

Aleph

Arithmetic

Basic

Continuum

CountableCover

Defs

ENat

Embedding

Finite

Finsupp

HasCardinalLT

NatCard

Order

Ordinal

Pigeonhole

Rat

Regular

SchroederBernstein

Subfield

ToNat

Descriptive

Tree

Ordinal

Arithmetic

Basic

Enum

Exponential

Family

FixedPoint

FundamentalSequence

Principal

Rank

Topology

Univ

ZFC

Basic

Cardinal

Class

Ordinal

PSet

Rank

VonNeumann

Tactic

ArithMult (file)

Init

Attr

Core

Register

Bound (file)

Attribute

Init

CancelDenoms

Core

CategoryTheory

Coherence

Basic

Datatypes

Normalize

PureCoherence

Monoidal

Basic

Datatypes

Normalize

PureCoherence

CancelIso

CategoryStar

Elementwise

IsoReassoc

MonoidalComp

Reassoc

Slice

ToApp

Continuity (file)

Init

FieldSimp (file)

Attr

Discharger

Lemmas

Finiteness (file)

Attr

FunProp (file)

Attr

Core

Decl

Elab

FunctionData

Mor

Theorems

ToBatteries

Types

GCongr (file)

Core

CoreAttrs

ForwardAttr

GRewrite (file)

Core

Elab

Linarith (file)

Oracle

SimplexAlgorithm (file)

Datatypes

Gauss

PositiveVector

SimplexAlgorithm

Datatypes

Frontend

Lemmas

Parsing

Preprocessing

Verification

LinearCombination (file)

Lemmas

Linter (file)

AuxLemma

DeprecatedSyntaxLinter

DirectoryDependency

DocPrime

DocString

EmptyLine

FlexibleLinter

GlobalAttributeIn

HashCommandLinter

HaveLetLinter

Header

Lint

MinImports

Multigoal

OldObtain

OverlappingInstances

PPRoundtrip

PrivateModule

Style

TacticDocumentation

UnusedInstancesInType

UnusedTactic

UnusedTacticExtension

UpstreamableDecl

Whitespace

Measurability (file)

Init

Monotonicity

Attr

Nontriviality (file)

Core

NormNum (file)

Abs

Basic

BigOperators

Core

DivMod

Eq

GCD

Ineq

Inv

LegendreSymbol

NatFactorial

NatFib

OfScientific

Parity

Pow

Prime

RealSqrt

Result

Order (file)

Graph

Basic

Tarjan

CollectFacts

Preprocessing

ToInt

Positivity (file)

Basic

Core

Finset

Push (file)

Attr

Relation

Rfl

Ring (file)

Basic

Common

Compare

NamePowerVars

PNat

RingNF

Simproc

ExistsAndEq

Simps

Basic

NotationClass

TacticAnalysis (file)

Declarations

Translate

Attributes

Core

GuessName

Reorder

TagUnfoldBoundary

ToAdditive

ToDual

UnfoldBoundary

Widget

Calc

CongrM

Conv

LibraryRewrite

SelectInsertParamsClass

SelectPanelUtils

Abel

AdaptationNote

Algebraize

ApplyAt

ApplyCongr

ApplyFun

ApplyWith

BDSimp

Basic

ByCases

ByContra

Cases

CasesM

Check

Choose

ClearExcept

ClearExclamation

Clear_

Coe

Common

ComputeDegree

CongrExclamation

CongrM

Constructor

ContinuousFunctionalCalculus

Contrapose

Conv

Convert

Core

CrossRefAttribute

DSimpPercent

DeclarationNames

DefEqAbuse

DefEqTransformations

DepRewrite

DeprecateTo

DeriveFintype

Eqns

ErwQuestion

Eval

ExistsI

Ext

ExtendDoc

ExtractGoal

FBinop

FailIfNoProgress

FastInstance

Field

FinCases

Find

Generalize

Group

GuardGoalNums

GuardHypNums

HaveI

HigherOrder

Hint

InferParam

Inhabit

IntervalCases

IrreducibleDef

Lemma

Lift

MinImports

MkIffOfInductiveProp

Module

MoveAdd

NoncommRing

NthRewrite

Observe

OfNat

PPWithUniv

Peel

Polyrith

ProxyType

Qify

RSuffices

Recover

Rename

RenameBVar

Rify

Says

ScopedNS

Set

SetLike

SimpIntro

SimpRw

SplitIfs

Spread

Subsingleton

Substs

SuccessIfFailWithMsg

SudoSetOption

SuppressCompilation

SwapVar

TFAE

Tauto

TautoSet

TermCongr

ToAdditive

ToDual

ToExpr

ToFun

ToLevel

Trace

TryThis

TypeStar

UnsetOption

Use

Variable

WLOG

Zify

Topology

Algebra

Algebra (file)

Equiv

Constructions (file)

DomMulAct

Group

Basic

ClosedSubgroup

Compact

Defs

GroupTopology

Matrix

Pointwise

Quotient

Torsor

InfiniteSum

Basic

ConditionalInt

Constructions

Defs

ENNReal

Field

Group

Module

NatInt

Order

Real

Ring

SummationFilter

TsumUniformlyOn

UniformOn

IsUniformGroup

Basic

Constructions

Defs

DiscreteSubgroup

Order

MetricSpace

Lipschitz

Module

Alternating

Basic

Topology

ContinuousLinearMap

Basic

Idempotent

PiProd

Quotient

Restrict

RestrictScalars

Multilinear

Basic

Bounded

Topology

Spaces

CharacterSpace

ContinuousLinearMap

PointwiseConvergenceCLM

UniformConvergenceCLM

WeakBilin

WeakDual

Basic

Cardinality

ClosedSubmodule

Complement

Determinant

Equiv

FiniteDimension

LocallyConvex

ModuleTopology

PerfectPairing

PerfectSpace

Simple

Star

TransferInstance

UniformConvergence

Monoid (file)

Defs

FunOnFinite

Nonarchimedean

AdicTopology

Bases

Basic

Order

Archimedean

ArchimedeanDiscrete

Field

Floor

Group

LiminfLimsup

Support

Ring

Basic

Ideal

Real

SeparationQuotient

Basic

FiniteDimensional

Section

Star (file)

Real

ValuativeRel

ValuativeTopology

Valued

ValuationTopology

ValuedField

WithVal

Affine

AffineSubspace

ConstMulAction

ContinuousAffineEquiv

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

LinearTopology

MulAction

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

StarSubalgebra

Support

TopologicallyNilpotent

UniformConvergence

UniformField

UniformFilterBasis

UniformMulAction

UniformRing

WithZeroTopology

Baire

BaireMeasurable

CompleteMetrizable

Lemmas

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Real

Category

TopCat

Limits

Basic

Konig

Products

Pullbacks

Adjunctions

Basic

EpiMono

OpenNhds

Opens

Compactification

OnePoint

Basic

ProjectiveLine

StoneCech

Compactness

Bases

Compact

CompactSystem

CompactlyCoherentSpace

Lindelof

LocallyCompact

LocallyFinite

NhdsKer

Paracompact

SigmaCompact

Connected

Basic

Clopen

LocPathConnected

LocallyConnected

PathConnected

TotallyDisconnected

Constructions (file)

SumProd

ContinuousMap

Bounded

Basic

Normed

Star

Algebra

Basic

CocompactMap

Compact

CompactlySupported

ContinuousMapZero

ContinuousSqrt

Defs

Ideals

Lattice

Ordered

Periodic

Polynomial

SecondCountableSpace

Star

StarOrdered

StoneWeierstrass

T0Sierpinski

Units

Weierstrass

ZeroAtInfty

Covering

AddCircle

Basic

Quotient

Defs

Basic

Filter

Induced

Sequences

Ultrafilter

EMetricSpace

Basic

BoundedVariation

Defs

Diam

Lipschitz

Paracompact

Pi

FiberBundle

Basic

Constructions

IsHomeomorphicTrivialBundle

Trivialization

GDelta

Basic

MetrizableSpace

Hom

ContinuousEval

ContinuousEvalConst

Homeomorph

Defs

Lemmas

Quotient

TransferInstance

Homotopy

Basic

Contractible

Equiv

HomotopyGroup

Path

Product

Instances

AddCircle

Defs

DenseSubgroup

Real

ENNReal

Lemmas

EReal

Lemmas

NNReal

Lemmas

Real

Lemmas

Discrete

ENat

Int

Matrix

Nat

Rat

RealVectorSpace

Shrink

Sign

ZMultiples

LocallyConstant

Basic

Maps

Proper

Basic

CompactlyGenerated

Strict

Basic

Basic

OpenQuotient

MetricSpace

ProperSpace (file)

Lemmas

Real

Pseudo

Basic

Constructions

Defs

Lemmas

Pi

Real

Ultra

Basic

Algebra

Antilipschitz

Basic

Bounded

CantorScheme

CauSeqFilter

Cauchy

Completion

Contracting

Defs

Dilation

DilationEquiv

Equicontinuity

Gluing

HausdorffDimension

HausdorffDistance

Holder

IsometricSMul

Isometry

Lipschitz

MetricSeparated

PartitionOfUnity

Perfect

PiNat

Polish

Sequences

ThickenedIndicator

Thickening

TransferInstance

UniformConvergence

Metrizable

Basic

CompletelyMetrizable

Real

Uniformity

Urysohn

OpenPartialHomeomorph

Basic

Composition

Constructions

Continuity

Defs

IsImage

Order (file)

AtTopBotIxx

Basic

Bornology

Compact

DenselyOrdered

ExtendFrom

ExtrClosure

IntermediateValue

IsLUB

IsLocallyClosed

IsNormal

Lattice

LeftRight

LeftRightLim

LeftRightNhds

LiminfLimsup

LocalExtr

LowerUpperTopology

Monotone

MonotoneContinuity

MonotoneConvergence

OrderClosed

ProjIcc

Real

Rolle

ScottTopology

SuccPred

T5

UpperLowerSetTopology

WithTop

PartialHomeomorph

Defs

Semicontinuity

Basic

Defs

Hemicontinuity

Separation

Basic

CompletelyRegular

CountableSeparatingOn

GDelta

Hausdorff

Regular

SeparatedNhds

Sets

Closeds

Compacts

OpenCover

Opens

Sheaves

SheafCondition

OpensLeCover

PairwiseIntersections

Sites

UniqueGluing

Forget

Functors

Init

LocallySurjective

PUnit

Presheaf

Sheaf

Skyscraper

Stalks

Spectral

Basic

Hom

Prespectral

UniformSpace

AbstractCompletion

Ascoli

Basic

Cauchy

Compact

CompactConvergence

CompleteSeparated

Completion

Defs

DiscreteUniformity

Equicontinuity

Equiv

HeineCantor

LocallyUniformConvergence

Matrix

OfFun

Pi

Real

Separation

UniformApproximation

UniformConvergence

UniformConvergenceTopology

UniformEmbedding

VectorBundle

Basic

Constructions

AlexandrovDiscrete

Bases

Basic

Clopen

Closure

ClusterPt

Coherent

CompactOpen

Constructible

Continuous

ContinuousOn

DenseEmbedding

DerivedSet

DiscreteSubset

ExtendFrom

IndicatorConstPointwise

Inseparable

Irreducible

IsClosedRestrict

IsLocalHomeomorph

KrullDimension

LocalAtTarget

LocallyClosed

LocallyFinite

LocallyFinsupp

Neighborhoods

NhdsKer

NhdsSet

NhdsWithin

NoetherianSpace

PartitionOfUnity

Path

Perfect

Piecewise

QuasiSeparated

SeparatedMap

Sequences

ShrinkingLemma

Sober

TietzeExtension

Ultrafilter

UnitInterval

UrysohnsBounded

UrysohnsLemma

WithTopology

Util

AtomM (file)

Recurse

AddRelatedDecl

AtLocation

CompileInductive

CountHeartbeats

DelabNonCanonical

Delaborators

DischargerAsTactic

ElabWithoutMVars

Notation3

PPOptions

ParseCommand

PrintSorries

Qq

Superscript

SynthesizeUsing

Tactic

TermReduce

TransImports

WhatsNew

WithWeakNamespace

Init

Plausible (file)

Arbitrary

ArbitraryFueled

Attr

DeriveArbitrary

DeriveShrinkable

Functions

Gen

Random

Sampleable

Shrinkable

Tactic

Testable

ProofWidgets

Component

Basic

FilterDetails

MakeEditLink

OfRpcMethod

Data

Html

Cancellable

Compat

Util

Qq (file)

ForLean

Do

ReduceEval

ToExpr

AssertInstancesCommute

Commands

Delab

Macro

Match

MatchImpl

MetaM

Simp

SortLocalDecls

Typ

Std (file)

Async (file)

Basic

ContextAsync

DNS

IO

Process

Select

Signal

System

TCP

Timer

UDP

Data (file)

DHashMap (file)

Internal

AssocList

Basic

Iterator

Lemmas

Defs

HashesTo

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawDef

RawLemmas

DTreeMap (file)

Internal

WF

Defs

Lemmas

Balanced

Balancing

Cell

Def

Lemmas

Model

Operations

Ordered

Queries

Zipper

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ExtDHashMap (file)

Basic

Lemmas

ExtDTreeMap (file)

Basic

Lemmas

ExtHashMap (file)

Basic

Lemmas

ExtHashSet (file)

Basic

Lemmas

ExtTreeMap (file)

Basic

Lemmas

ExtTreeSet (file)

Basic

Lemmas

HashMap (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

HashSet (file)

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

Internal

List

Associative

Defs

Cut

Iterators (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

StepSize

TakeWhile

Zip

Drop

DropWhile

StepSize

TakeWhile

Zip

Consumers (file)

Monadic (file)

Set

Set

Lemmas (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

FilterMap

TakeWhile

Zip

Drop

DropWhile

TakeWhile

Zip

Consumers (file)

Monadic (file)

Collect

Loop

Set

Collect

Loop

Set

Equivalence (file)

Basic

HetT

StepCongr

Producers (file)

Monadic (file)

Array

Empty

List

Vector

Array

Empty

Range

Repeat

Slice

Vector

Monadic

Producers (file)

Monadic (file)

Array

Empty

Vector

Array

Empty

Range

Repeat

Slice

Vector

String (file)

ToInt

ToNat

TreeMap (file)

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

TreeSet (file)

Raw (file)

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ByteSlice

Do (file)

Internal (file)

Ensures (file)

Def

Lemmas

SPred (file)

Notation (file)

Basic

DerivedLaws

Laws

SPred

SVal

Triple (file)

Basic

SpecLemmas

WP (file)

Basic

Monad

SimpLemmas

Sound

PostCond

PredTrans

Http (file)

Data (file)

Body (file)

Any

Basic

Empty

Full

Length

Stream

Headers (file)

Basic

Name

Value

URI (file)

Basic

Config

Encoding

Parser

Chunk

Extensions

Method

Request

Response

Status

Version

Internal (file)

Char

ChunkedBuffer

Encode

IndexMultiMap

LowerCase

String

Protocol

H1 (file)

Config

Error

Event

Message

Parser

Reader

Writer

Server (file)

Config

Connection

Handler

Test

Helpers

Transport

Internal (file)

Do (file)

Order

Basic

Frame

Lemmas

Triple (file)

Basic

Gadget

SpecLemmas

WP (file)

Basic

Lemmas

Assertion

ExceptPost

PredTrans

Parsec (file)

Basic

ByteArray

String

UV (file)

DNS

Loop

Signal

System

TCP

Timer

UDP

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

Broadcast

CancellationContext

CancellationToken

Channel

Mutex

Notify

RecursiveMutex

Semaphore

SharedMutex

StreamMap

Tactic (file)

BVDecide (file)

Bitblast (file)

BVExpr (file)

Circuit (file)

Impl (file)

Operations

Add

Append

Clz

Cpop

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

Reverse

RotateLeft

RotateRight

ShiftLeft

ShiftRight

Sub

Udiv

Ult

Umod

ZeroExtend

Carry

Const

Expr

Pred

Substructure

Var

Lemmas (file)

Operations

Add

Append

Clz

Cpop

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

Reverse

RotateLeft

RotateRight

ShiftLeft

ShiftRight

Sub

Udiv

Ult

Umod

ZeroExtend

Basic

Carry

Const

Expr

Pred

Var

Basic

BoolExpr (file)

Basic

LRAT (file)

Internal

Formula (file)

Class

Implementation

Instance

Lemmas

RatAddResult

RatAddSound

RupAddResult

RupAddSound

Actions

Assignment

CNF

Clause

CompactLRATChecker

CompactLRATCheckerSound

Convert

Entails

LRATChecker

LRATCheckerSound

PosFin

Actions

Checker

Parser

Normalize (file)

BitVec

Bool

Canonicalize

Equal

Prop

Reflect

Syntax

Do (file)

ProofMode

Syntax

Time (file)

Date (file)

Unit

Basic

Day

Month

Week

Weekday

Year

Basic

PlainDate

ValidDate

DateTime (file)

PlainDateTime

Timestamp

WallTime

Format (file)

Basic

DateFormat

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

TimeZone

ZoneRules

Duration

Color scheme

darksystemlight