General documentation

index

foundational types

references

Library

Aesop (file)

Builder

Apply

Basic

Cases

Constructors

Default

Forward

NormSimp

Tactic

Unfold

BuiltinRules (file)

ApplyHyps

Assumption

DestructProducts

Ext

Intros

Rfl

Split

Subst

Forward

Match (file)

Types

State (file)

ApplyGoalDiff

Initial

LevelIndex

PremiseIndex

RuleInfo

SlotIndex

Substitution

Frontend

Extension (file)

Init

Attribute

Basic

Command

RuleExpr

Saturate

Tactic

Index (file)

Basic

DiscrTreeConfig

Forward

RulePattern

Options (file)

Internal

Public

RPINF (file)

Basic

Rule (file)

Basic

Forward

Name

RulePattern (file)

Cache

RuleSet (file)

Filter

Member

Name

RuleTac (file)

Forward (file)

Basic

Apply

Basic

Cases

Descr

ElabRuleTerm

FVarIdSubst

GoalDiff

Preprocess

RuleTerm

Tactic

Script

Check

CtorNames

GoalWithMVars

Main

OptimizeSyntax

SScript

ScriptM

SpecificTactics

Step

StructureDynamic

StructureStatic

Tactic

TacticState

UScript

UScriptToSScript

Util

Search

Expansion (file)

Basic

Norm

Simp

Queue (file)

Class

ExpandSafePrefix

Main

RuleSelection

SearchM

Stats

Basic

Extension

Report

Tree (file)

Data (file)

ForwardRuleMatches

AddRapp

Check

ExtractProof

ExtractScript

Free

RunMetaM

State

Tracing

Traversal

TreeM

UnsafeQueue

Util

Tactic (file)

Ext

Unfold

Basic

EqualUpToIds

UnionFind

UnorderedArraySet

BaseM

Check

Constants

ElabM

Exception

Main

Nanos

Percent

Saturate

Tracing

Archive (file)

Examples

IfNormalization

Result

Statement

WithoutAesop

Eisenstein

MersennePrimes

PropEncodable

Imo

Imo1959Q1

Imo1959Q2

Imo1960Q1

Imo1960Q2

Imo1961Q3

Imo1962Q1

Imo1962Q4

Imo1963Q5

Imo1964Q1

Imo1969Q1

Imo1972Q5

Imo1975Q1

Imo1977Q6

Imo1981Q3

Imo1982Q1

Imo1982Q3

Imo1985Q2

Imo1986Q5

Imo1987Q1

Imo1988Q6

Imo1994Q1

Imo1998Q2

Imo2001Q2

Imo2001Q3

Imo2001Q6

Imo2005Q3

Imo2005Q4

Imo2006Q3

Imo2006Q5

Imo2008Q2

Imo2008Q3

Imo2008Q4

Imo2011Q3

Imo2011Q5

Imo2013Q1

Imo2013Q5

Imo2015Q6

Imo2019Q1

Imo2019Q2

Imo2019Q4

Imo2020Q2

Imo2021Q1

Imo2024Q1

Imo2024Q2

Imo2024Q3

Imo2024Q5

Imo2024Q6

MiuLanguage

Basic

DecisionNec

DecisionSuf

OxfordInvariants

Summer2021

Week3P1

Wiedijk100Theorems

AbelRuffini

AreaOfACircle

AscendingDescendingSequences

BallotProblem

BirthdayProblem

BuffonsNeedle

CubingACube

FriendshipGraphs

HeronsFormula

InverseTriangleSum

Konigsberg

Partition

PerfectNumbers

SolutionOfCubicQuartic

SumOfPrimeReciprocalsDiverges

Arithcc

Hairer

Sensitivity

ZagierTwoSquares

Batteries (file)

Classes

Cast

Order

RatCast

SatisfiesM

CodeAction (file)

Attr

Basic

Deprecated

Misc

Control

ForInStep (file)

Basic

Lemmas

Nondet

Basic

AlternativeMonad

Lemmas

Monad

OptionT

Data

Array (file)

Init

Lemmas

Basic

Lemmas

Match

Merge

Monadic

OfFn

Pairwise

BinomialHeap (file)

Basic

Lemmas

BitVec (file)

Basic

Lemmas

DList (file)

Basic

Lemmas

Fin (file)

Basic

Fold

Lemmas

OfBits

HashMap (file)

Basic

Lemmas

List (file)

Init

Lemmas

ArrayMap

Basic

Count

Lemmas

Matcher

Monadic

OfFn

Pairwise

Perm

MLList (file)

Basic

Heartbeats

IO

Nat (file)

Basic

Bisect

Gcd

Lemmas

RBMap (file)

Alter

Basic

Depth

Lemmas

WF

Random (file)

MersenneTwister

Range (file)

Lemmas

Rat (file)

Basic

Float

Lemmas

String (file)

Basic

Lemmas

Matcher

UnionFind (file)

Basic

Lemmas

Vector (file)

Basic

Lemmas

Monadic

AssocList

BinaryHeap

ByteArray

ByteSubarray

Char

FloatArray

Int

NameSet

PairingHeap

Stream

UInt

Lean

IO

Process

Meta

Basic

DiscrTree

Expr

Inaccessible

InstantiateMVars

SavedState

Simp

UnusedNames

System

IO

Util

EnvSearch

AttributeExtra

EStateM

Except

Expr

Float

HashMap

HashSet

Json

LawfulMonad

LawfulMonadLift

MonadBacktrack

NameMapAttribute

PersistentHashMap

PersistentHashSet

Position

SatisfiesM

Syntax

TagAttribute

Linter (file)

UnnecessarySeqFocus

UnreachableTactic

Tactic

Lint (file)

Basic

Frontend

Misc

Simp

TypeClass

Alias

Basic

Case

Congr

Exact

HelpCmd

Init

Instances

Lemma

NoMatch

OpenPrivate

PermuteGoals

PrintDependents

PrintOpaques

PrintPrefix

SeqFocus

ShowUnused

SqueezeScope

Trans

Unreachable

Util

Cache

ExtendedBinder

LibraryNote

Panic

Pickle

ProofWanted

Logic

WF

Counterexamples (file)

AharoniKorman

CanonicallyOrderedCommSemiringTwoMul

CharPZeroNeCharZero

CliffordAlgebraNotInjective

Cyclotomic105

DirectSumIsInternal

DiscreteTopologyNonDiscreteUniformity

GameMultiplication

Girard

HomogeneousPrimeNotPrime

IrrationalPowerOfIrrational

LinearOrderWithPosMulPosEqZero

MapFloor

MonicNonRegular

OrderedCancelAddCommMonoidWithBounds

Phillips

Pseudoelement

QuadraticForm

SeminormLatticeNotDistrib

SorgenfreyLine

ZeroDivisorsInAddMonoidAlgebras

ImportGraph

Imports

RequiredModules

Init (file)

Control (file)

Lawful (file)

MonadLift (file)

Basic

Instances

Lemmas

Basic

Instances

Lemmas

Basic

EState

Except

ExceptCps

Id

Option

Reader

State

StateCps

StateRef

Data (file)

Array (file)

Lex (file)

Basic

Lemmas

QSort (file)

Basic

Subarray (file)

Split

Attach

Basic

BasicAux

BinSearch

Bootstrap

Count

DecidableEq

Erase

Extract

FinRange

Find

GetLit

InsertIdx

InsertionSort

Lemmas

MapIdx

Mem

Monadic

OfFn

Perm

Range

Set

TakeDrop

Zip

BitVec (file)

Basic

BasicAux

Bitblast

Bootstrap

Decidable

Folds

Lemmas

ByteArray (file)

Basic

Char (file)

Basic

Lemmas

Fin (file)

Basic

Bitwise

Fold

Iterate

Lemmas

Log2

FloatArray (file)

Basic

Format (file)

Basic

Instances

Macro

Syntax

Int (file)

Bitwise (file)

Basic

Lemmas

DivMod (file)

Basic

Bootstrap

Lemmas

Basic

Compare

Cooper

Gcd

Lemmas

LemmasAux

Linear

OfNat

Order

Pow

Iterators (file)

Combinators (file)

Monadic (file)

Attach

FilterMap

ULift

Attach

FilterMap

ULift

Consumers (file)

Monadic (file)

Access

Collect

Loop

Partial

Access

Collect

Loop

Partial

Internal (file)

LawfulMonadLiftFunction

Termination

Lemmas (file)

Combinators (file)

Monadic (file)

Attach

FilterMap

ULift

Attach

FilterMap

ULift

Consumers (file)

Monadic (file)

Collect

Loop

Collect

Loop

Monadic

Basic

Basic

Basic

PostconditionMonad

ToIterator

List (file)

Nat (file)

BEq

Basic

Count

Erase

Find

InsertIdx

Modify

Pairwise

Perm

Range

Sublist

TakeDrop

Sort (file)

Basic

Impl

Lemmas

Attach

Basic

BasicAux

Control

Count

Erase

FinRange

Find

Impl

Lemmas

Lex

MapIdx

MinMax

Monadic

Notation

OfFn

Pairwise

Perm

Range

Sublist

TakeDrop

ToArray

ToArrayImpl

Zip

Nat (file)

Bitwise (file)

Basic

Lemmas

Div (file)

Basic

Lemmas

Basic

Compare

Control

Dvd

Fold

Gcd

Lcm

Lemmas

Linear

Log2

MinMax

Mod

Power2

SOM

Simproc

Option (file)

Array

Attach

Basic

BasicAux

Coe

Instances

Lemmas

List

Monadic

Range (file)

Polymorphic (file)

Basic

Iterators

Lemmas

Nat

NatLemmas

PRange

RangeIterator

UpwardEnumerable

Basic

Lemmas

SInt (file)

Basic

Bitwise

Float

Float32

Lemmas

Slice (file)

Array (file)

Basic

Iterator

Lemmas

Basic

Lemmas

Notation

Operations

String (file)

Basic

Extra

Lemmas

Sum (file)

Basic

Lemmas

ToString (file)

Basic

Macro

UInt (file)

Basic

BasicAux

Bitwise

Lemmas

Log2

Vector (file)

Attach

Basic

Count

DecidableEq

Erase

Extract

FinRange

Find

InsertIdx

Lemmas

Lex

MapIdx

Monadic

OfFn

Perm

Range

Zip

AC

BEq

Basic

Bool

Cast

Float

Float32

Function

Hashable

NeZero

OfScientific

Ord

PLift

Prod

Queue

RArray

Random

Repr

Stream

Subtype

ULift

Zero

Grind (file)

Module (file)

Basic

Envelope

Ordered (file)

Field

Int

Linarith

Module

Order

Ring

Ring (file)

Basic

Envelope

Field

OfSemiring

Poly

ToInt

Attr

Cases

Ext

Lemmas

Norm

Offset

PP

Propagator

Tactics

ToInt

ToIntLemmas

Util

GrindInstances (file)

Ring (file)

BitVec

Fin

Int

Nat

SInt

UInt

Nat

ToInt

Internal (file)

Order (file)

Basic

Lemmas

Tactic

Omega (file)

Coeffs

Constraint

Int

IntList

LinearCombo

Logic

System (file)

FilePath

IO

IOError

Mutex

Platform

Promise

ST

Uri

BinderNameHint

BinderPredicates

ByCases

Classical

Coe

Conv

Core

Dynamic

Ext

GetElem

Guard

Hints

MacroTrace

Meta

MetaTypes

Notation

NotationExtra

Prelude

PropLemmas

RCases

ShareCommon

SimpLemmas

Simproc

SizeOf

SizeOfLemmas

Syntax

Tactics

TacticsExtra

Task

Try

Util

WF

WFTactics

While

Lake (file)

Build (file)

Job (file)

Basic

Monad

Register

Target (file)

Basic

Fetch

Actions

Common

Context

Data

Facets

Fetch

Index

Info

Key

Library

Module

ModuleArtifacts

Package

Run

Store

Targets

Topological

Trace

CLI

Actions

Build

Error

Config (file)

Artifact

Cache

ConfigDecl

ConfigTarget

Context

Defaults

Dependency

Dynlib

Env

ExternLib

ExternLibConfig

FacetConfig

Glob

InputFile

InputFileConfig

InstallPath

Kinds

LeanConfig

LeanExe

LeanExeConfig

LeanLib

LeanLibConfig

Meta

Module

Monad

Opaque

OutFormat

Package

Pattern

Script

TargetConfig

Workspace

WorkspaceConfig

DSL (file)

Attributes

AttributesCore

Config

DeclUtil

Extensions

Key

Meta

Package

Require

Script

Syntax

Targets

VerLit

Load

Config

Manifest

Toml (file)

Data

DateTime

Dict

Value

Elab (file)

Expression

Value

Grammar

Load

ParserUtil

Util

Binder

Casing

Compare

Cycle

DRBMap

Date

EStateT

EquipT

Error

Exit

Family

FilePath

Git

IO

JsonObject

Lift

List

Lock

Log

Message

Name

NativeLib

Opaque

OpaqueType

OrdHashSet

OrderedTagAttribute

Proc

RBArray

Store

StoreInsts

Sugar

Task

Version

Reservoir

Version

Lean (file)

Compiler (file)

IR (file)

Basic

Borrow

Boxing

Checker

CompilerM

ElimDeadBranches

ElimDeadVars

EmitC

EmitLLVM

EmitUtil

ExpandResetReuse

Format

FreeVars

LLVMBindings

LiveVars

NormIds

PushProj

RC

ResetReuse

SimpCase

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

CompatibleTypes

CompilerM

ConfigOptions

DeclHash

DependsOn

ElimDead

ElimDeadBranches

ExtractClosed

FVarUtil

FixedParams

FloatLetIn

InferType

Internalize

JoinPoints

LCtx

LambdaLifting

Level

Main

MonadScope

MonoTypes

OtherDecl

PassManager

Passes

PhaseExt

PrettyPrinter

Probing

PullFunDecls

PullLetDecls

ReduceArity

ReduceJpArity

Renaming

ScopeM

SpecInfo

Specialize

StructProjCases

Testing

ToDecl

ToExpr

ToLCNF

ToMono

Types

Util

AtMostOnce

BorrowedAnnotation

CSimpAttr

ClosedTermCache

ConstFolding

ExportAttr

ExternAttr

FFI

ImplementedByAttr

InitAttr

InlineAttrs

Main

MetaAttr

NameMangling

NeverExtractAttr

NoncomputableAttr

Old

Options

Specialize

Data (file)

Json (file)

Basic

Elab

FromToJson

Parser

Printer

Stream

Lsp (file)

Basic

CancelParams

Capabilities

Client

CodeActions

Communication

Diagnostics

Extra

InitShutdown

Internal

Ipc

LanguageFeatures

TextSync

Utf16

Window

Workspace

Xml (file)

Basic

Parser

Array

AssocList

DeclarationRange

Format

FuzzyMatching

JsonRpc

KVMap

LBool

LOption

Name

NameMap

NameTrie

OpenDecl

Options

PersistentArray

PersistentHashMap

PersistentHashSet

Position

PrefixTree

RArray

RBMap

RBTree

SMap

SSet

Trie

DocString (file)

Add

Extension

Links

Elab (file)

Deriving (file)

BEq

Basic

DecEq

FromToJson

Hashable

Inhabited

Nonempty

Ord

Repr

SizeOf

ToExpr

TypeName

Util

InfoTree (file)

InlayHints

Main

Types

PreDefinition (file)

Nonrec

Eqns

PartialFixpoint (file)

Eqns

Induction

Main

Structural (file)

BRecOn

Basic

Eqns

FindRecArg

IndGroupInfo

IndPred

Main

Preprocess

RecArgInfo

SmartUnfolding

WF (file)

Basic

Eqns

Fix

FloatRecApp

GuessLex

Main

PackMutual

Preprocess

Rel

Unfold

Basic

EqUnfold

Eqns

FixedParams

Main

MkInhabitant

Mutual

TerminationHint

TerminationMeasure

Quotation (file)

Precheck

Util

Tactic (file)

BVDecide (file)

Frontend (file)

BVDecide (file)

Reflect

ReifiedBVExpr

ReifiedBVLogical

ReifiedBVPred

ReifiedLemmas

Reify

SatAtBVLogical

Normalize (file)

AC

AndFlatten

ApplyControlFlow

Basic

EmbeddedConstraint

Enums

IntToBitVec

Rewrite

ShortCircuit

Simproc

Structures

TypeAnalysis

Attr

BVCheck

BVTrace

LRAT

LRAT (file)

Trim

External

Conv (file)

Basic

Change

Congr

Delta

Lets

Pattern

Rewrite

Simp

Unfold

Do (file)

ProofMode (file)

Assumption

Basic

Cases

Clear

Constructor

Delab

Exact

Exfalso

Focus

Frame

Have

Intro

LeftRight

MGoal

Pure

Refine

Revert

Specialize

Attr

LetElim

Spec

Syntax

VCGen

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

AsAuxLemma

Basic

BoolToPropSimps

BuiltinTactic

Calc

Change

Classical

Config

Congr

Delta

DiscrTreeKey

Doc

ElabTerm

ExposeNames

Ext

FalseOrByContra

Generalize

Grind

Guard

Induction

Injection

Lets

LibrarySearch

Location

Match

Meta

Monotonicity

NormCast

RCases

Repeat

Rewrite

Rewrites

Rfl

Show

ShowTerm

Simp

SimpArith

SimpTrace

Simpa

Simproc

SolveByElim

Split

Symm

TreeTacAttr

Try

Unfold

App

Arg

Attributes

AutoBound

AuxDef

BinderPredicates

Binders

BindersUtil

BuiltinCommand

BuiltinEvalCommand

BuiltinNotation

BuiltinTerm

Calc

CheckTactic

Command

ComputedFields

Config

DeclModifiers

DeclNameGen

DeclUtil

Declaration

DeclarationRange

DefView

Do

ElabRules

ErrorExplanation

Eval

Exception

Extra

Frontend

GenInjective

GuardMsgs

Import

Inductive

InfoTrees

InheritDoc

LetRec

Level

Macro

MacroArgUtil

MacroRules

Match

MatchAltView

MatchExpr

Mixfix

MutualDef

MutualInductive

Notation

Open

ParseImportsFast

PatternVar

Print

RecAppSyntax

RecommendedSpelling

SetOption

StructInst

Structure

Syntax

SyntheticMVars

Term

Time

Util

WhereFinally

ErrorExplanations (file)

CtorResultingTypeMismatch

DependsOnNoncomputable

InductiveParamMismatch

InductiveParamMissing

InvalidDottedIdent

RedundantMatchAlt

Language

Lean (file)

Types

Basic

Util

Linter (file)

Basic

Builtin

ConstructorAsVariable

Deprecated

List

MissingDocs

Omit

Sets

UnusedSimpArgs

UnusedVariables

Util

Meta (file)

ArgsPacker (file)

Basic

Constructions (file)

BRecOn

CasesOn

NoConfusion

NoConfusionLinear

RecOn

Match (file)

MatcherApp (file)

Basic

Transform

Basic

CaseArraySizes

CaseValues

MVarRenaming

Match

MatchEqs

MatchEqsExt

MatchPatternAttr

MatcherInfo

Value

Tactic (file)

AC (file)

Main

Grind (file)

Arith (file)

CommRing (file)

DenoteExpr

EqCnstr

Internalize

Inv

PP

Poly

Proof

Reify

RingId

SafePoly

ToExpr

Types

Util

Var

Cutsat (file)

CommRing

DvdCnstr

EqCnstr

Inv

LeCnstr

MBTC

Model

Nat

Norm

Proof

ReorderVars

Search

SearchM

ToInt

ToIntInfo

Types

Util

Var

Linear (file)

DenoteExpr

IneqCnstr

Internalize

Inv

MBTC

Model

PP

Proof

PropagateEq

Reify

Search

SearchM

StructId

ToExpr

Types

Util

Var

Offset (file)

Main

Model

Proof

Types

Util

Internalize

Inv

Main

Model

ModelUtil

ProofUtil

Simproc

Types

Util

AlphaShareCommon

Attr

Beta

Canon

Cases

CasesMatch

Core

Ctor

Diseq

EMatch

EMatchTheorem

EqResolution

ExprPtr

Ext

ExtAttr

ForallProp

Injection

Internalize

Intro

Inv

LawfulEqCmp

Lookahead

MBTC

Main

MarkNestedProofs

MatchCond

MatchDiscrOnly

PP

Parser

Proj

Proof

Propagate

PropagatorAttr

ProveEq

ReflCmp

RevertAll

SearchM

Simp

SimpUtil

Solve

Split

Types

Util

Simp (file)

Arith (file)

Int (file)

Basic

Simp

Nat (file)

Basic

Simp

Util

BuiltinSimprocs (file)

Array

BitVec

Char

Core

Fin

Int

List

Nat

SInt

String

UInt

Util

Attr

Diagnostics

LoopProtection

Main

RegisterCommand

Rewrite

SimpAll

SimpCongrTheorems

SimpTheorems

Simproc

Types

Try (file)

Collect

Acyclic

Apply

Assert

Assumption

AuxLemma

Backtrack

Cases

Cleanup

Clear

Congr

Constructor

Contradiction

Delta

ElimInfo

ExposeNames

Ext

FVarSubst

FunInd

FunIndCollect

FunIndInfo

Generalize

IndependentOf

Induction

Injection

Intro

Lets

LibrarySearch

NormCast

Refl

Rename

Repeat

Replace

Revert

Rewrite

Rewrites

Rfl

SolveByElim

Split

SplitIf

Subst

Symm

TryThis

Unfold

UnifyEq

Util

ACLt

AbstractMVars

AbstractNestedProofs

AppBuilder

Basic

BinderNameHint

Canonicalizer

Check

CheckTactic

Closure

Coe

CoeAttr

CollectFVars

CollectMVars

CompletionName

CongrTheorems

CtorRecognizer

DecLevel

Diagnostics

DiscrTree

DiscrTreeTypes

Eqns

Eval

ExprDefEq

ExprLens

ExprTraverse

ForEachExpr

FunInfo

GeneralizeTelescope

GeneralizeVars

GetUnfoldableConst

GlobalInstances

Hint

IndPredBelow

Inductive

InferType

Injective

Instances

IntInstTesters

Iterator

KAbstract

KExprMap

LazyDiscrTree

LetToHave

LevelDefEq

LitValues

MatchUtil

NatInstTesters

Offset

Order

PPGoal

PProdN

RecursorInfo

Reduce

ReduceEval

SizeOf

Sorry

Structure

SynthInstance

Transform

TransparencyMode

TryThis

UnificationHint

WHNF

Parser (file)

Tactic (file)

Doc

Term (file)

Doc

Attr

Basic

Command

Do

Extension

Extra

Level

Module

StrInterpolation

Syntax

Types

ParserCompiler (file)

Attribute

PrettyPrinter (file)

Delaborator (file)

Attributes

Basic

Builtins

FieldNotation

Options

SubExpr

TopDownAnalyze

Basic

Formatter

Parenthesizer

Server (file)

CodeActions (file)

Attr

Basic

Provider

UnknownIdentifier

Completion (file)

CompletionCollectors

CompletionInfoSelection

CompletionItemData

CompletionResolution

CompletionUtils

EligibleHeaderDecls

ImportCompletion

SyntheticCompletion

FileWorker (file)

ExampleHover

InlayHints

RequestHandling

SemanticHighlighting

SetupFile

SignatureHelp

Utils

WidgetRequests

Rpc (file)

Basic

Deriving

RequestHandling

Test (file)

Cancel

Runner

AsyncList

FileSource

GoTo

InfoUtils

References

RequestCancellation

Requests

ServerTask

Snapshots

Utils

Watchdog

Util (file)

CollectAxioms

CollectFVars

CollectLevelMVars

CollectLevelParams

CollectLooseBVars

CollectMVars

Diff

FVarSubset

FindExpr

FindLevelMVar

FindMVar

FoldConsts

ForEachExpr

ForEachExprWhere

HasConstCache

Heartbeats

InstantiateLevelParams

LakePath

LeanOptions

MonadBacktrack

MonadCache

NumApps

NumObjs

OccursCheck

PPExt

Path

Profile

Profiler

PtrSet

RecDepth

Recognizers

ReplaceExpr

ReplaceLevel

SCC

SafeExponentiation

SearchPath

ShareCommon

Sorry

SortExprs

TestExtern

Trace

Widget (file)

Basic

Diff

InteractiveCode

InteractiveDiagnostic

InteractiveGoal

TaggedText

Types

UserWidget

AddDecl

Attributes

AuxRecursor

BuiltinDocAttr

Class

CoreM

Declaration

DeclarationRange

DefEqAttrib

EnvExtension

Environment

ErrorExplanation

Exception

Expr

HeadIndex

Hygiene

ImportingFlag

InternalExceptionId

KeyedDeclsAttribute

LabelAttribute

Level

LoadDynlib

LocalContext

Log

Message

MetavarContext

Modifiers

MonadEnv

Namespace

PremiseSelection

PrivateName

ProjFns

ReducibilityAttrs

Replay

ReservedNameAction

ResolveName

Runtime

ScopedEnvExtension

Setup

Shell

Structure

SubExpr

Syntax

ToExpr

ToLevel

LeanSearchClient (file)

Basic

LoogleSyntax

Syntax

Mathlib (file)

Algebra

AddConstMap

Basic

Equiv

AddTorsor

Basic

Defs

Algebra

Hom (file)

Rat

Spectrum

Basic

Pi

Quasispectrum

Subalgebra

Basic

Centralizer

Directed

IsSimpleOrder

Lattice

MulOpposite

Operations

Order

Pi

Pointwise

Prod

Rank

Tower

Unitization

Basic

Bilinear

Defs

Equiv

Field

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Rat

RestrictScalars

Shrink

Tower

TransferInstance

Unitization

ZMod

Azumaya

Basic

Defs

Matrix

BigOperators

Finsupp

Basic

Fin

Group

Finset

Basic

Defs

Indicator

Lemmas

Pi

Piecewise

Powerset

Preimage

Sigma

List

Basic

Defs

Lemmas

Multiset

Basic

Defs

GroupWithZero

Action

Finset

Ring

Finset

List

Multiset

Nat

Associated

Balance

Expect

Field

Fin

Finprod

Intervals

Module

NatAntidiagonal

Option

Pi

RingEquiv

Sym

WithTop

BrauerGroup

Defs

Category

AlgCat

Basic

Limits

Monoidal

Symmetric

AlgebraCat

Symmetric

BialgCat

Basic

Monoidal

CoalgCat

Basic

ComonEquivalence

Monoidal

CommAlgCat

Basic

FiniteType

Monoidal

ContinuousCohomology

Basic

FGModuleCat

Basic

EssentiallySmall

Limits

Grp

AB

Abelian

Adjunctions

Basic

Biproducts

CartesianMonoidal

ChosenFiniteProducts

Colimits

EnoughInjectives

EpiMono

EquivalenceGroupAddGroup

FilteredColimits

FiniteGrp

ForgetCorepresentable

Images

Injective

IsFinite

Kernels

LargeColimits

LeftExactFunctor

Limits

Preadditive

Subobject

Ulift

Yoneda

ZModuleEquivalence

Zero

HopfAlgCat

Basic

Monoidal

ModuleCat

Differentials

Basic

Presheaf

Monoidal

Basic

Closed

Symmetric

Presheaf (file)

Abelian

ChangeOfRings

Colimits

EpiMono

Free

Generator

Limits

Monoidal

Pullback

Pushforward

Sheafification

Sheafify

Sheaf (file)

Abelian

ChangeOfRings

Colimits

Free

Generators

Limits

PullbackContinuous

PushforwardContinuous

Quasicoherent

Topology

Basic

Homology

AB

Abelian

Adjunctions

Algebra

Basic

Biproducts

ChangeOfRings

Colimits

EnoughInjectives

EpiMono

ExteriorPower

FilteredColimits

Free

Images

Injective

Kernels

Limits

Products

Projective

Pseudofunctor

Simple

Subobject

Tannaka

MonCat

Adjunctions

Basic

Colimits

FilteredColimits

ForgetCorepresentable

Limits

Yoneda

Ring

Under

Basic

Limits

Adjunctions

Basic

Colimits

Constructions

Epi

FilteredColimits

FinitePresentation

Instances

Limits

LinearAlgebra

Topology

Semigrp

Basic

BoolRing

GrpWithZero

Central

Basic

Defs

Matrix

TensorProduct

CharP

Algebra

Basic

CharAndCard

Defs

Frobenius

IntermediateField

Invertible

Lemmas

LinearMaps

LocalRing

MixedCharZero

Pi

Quotient

Reduced

Subring

Two

CharZero

Defs

Infinite

Quotient

Colimit

DirectLimit

Finiteness

Module

Ring

TensorProduct

ContinuedFractions

Computation

ApproximationCorollaries

Approximations

Basic

CorrectnessTerminating

TerminatesIffRat

Translations

Basic

ContinuantsRecurrence

ConvergentsEquiv

Determinant

TerminatedStable

Translations

DirectSum

AddChar

Algebra

Basic

Decomposition

Finsupp

Idempotents

Internal

LinearMap

Module

Ring

Divisibility

Basic

Finite

Hom

Prod

Units

EuclideanDomain

Basic

Defs

Field

Int

Field

Action

ConjAct

Subfield

Basic

Defs

Basic

Defs

Equiv

IsField

MinimalAxioms

NegOnePow

Opposite

Periodic

Power

Rat

Shrink

TransferInstance

ULift

ZMod

FreeAbelianGroup

Finsupp

UniqueSums

FreeAlgebra (file)

Cardinality

FreeMonoid

Basic

Count

Symbols

UniqueProds

GCDMonoid

Basic

Finset

IntegrallyClosed

Multiset

Nat

PUnit

Group

Action

Pointwise

Set

Basic

Finite

Finset

Basic

Defs

End

Equidecomp

Faithful

Hom

Opposite

Option

Pi

Pretransitive

Prod

Sigma

Sum

TypeTags

Units

Commute

Basic

Defs

Hom

Units

Equiv

Basic

Defs

Finite

Opposite

TypeTags

Fin

Basic

Tuple

Hom

Basic

CompTypeclasses

Defs

End

Instances

Int

Defs

Even

TypeTags

Units

Invertible

Basic

Defs

Irreducible

Defs

Lemmas

Nat

Defs

Even

Hom

Range

TypeTags

Units

Pi

Basic

Lemmas

Units

Pointwise

Finset

Basic

BigOperators

Density

Interval

Scalar

Set

Basic

BigOperators

Card

Finite

Lattice

ListOfFn

Scalar

Semiconj

Basic

Defs

Units

Subgroup

ZPowers

Basic

Lemmas

Actions

Basic

Defs

Even

Finite

Finsupp

Ker

Lattice

Map

MulOpposite

MulOppositeLemmas

Order

Pointwise

Submonoid

Basic

BigOperators

Defs

DistribMulAction

Finsupp

Membership

MulAction

MulOpposite

Operations

Pointwise

Units

Subsemigroup

Basic

Defs

Membership

Operations

TypeTags

Basic

Finite

Hom

UniqueProds

Basic

VectorSpace

Units

Basic

Defs

Equiv

Hom

Opposite

WithOne

Basic

Defs

AddChar

Basic

Center

Commutator

Conj

ConjFinite

Defs

Embedding

End

Even

EvenFunction

Ext

FiniteSupport

Finsupp

ForwardDiff

Graph

Idempotent

Indicator

InjSurj

MinimalAxioms

NatPowAssoc

Opposite

PNatPowAssoc

PUnit

Prod

Shrink

Support

Torsion

TransferInstance

Translate

ULift

GroupWithZero

Action

Pointwise

Finset

Set

Basic

Center

ConjAct

Defs

End

Faithful

Opposite

Pi

Prod

Units

Pointwise

Set

Basic

Card

Finset

Submonoid

Pointwise

Primal

Units

Basic

Equiv

Lemmas

Associated

Basic

Center

Commute

Conj

Defs

Divisibility

Equiv

Hom

Idempotent

Indicator

InjSurj

Int

Invertible

Nat

NeZero

NonZeroDivisors

Opposite

Pi

Prod

ProdHom

Range

Regular

Semiconj

Shrink

Subgroup

TransferInstance

ULift

WithZero

Homology

DerivedCategory

Ext

Basic

EnoughInjectives

EnoughProjectives

ExactSequences

ExtClass

Basic

ExactFunctor

Fractions

FullyFaithful

HomologySequence

ShortExact

SingleTriangle

Embedding

Basic

Boundary

CochainComplex

Connect

Extend

ExtendHomology

HomEquiv

IsSupported

Restriction

RestrictionHomology

StupidTrunc

TruncGE

TruncGEHomology

TruncLE

TruncLEHomology

Factorizations

Basic

HomotopyCategory (file)

DegreewiseSplit

HomComplex

HomComplexShift

HomologicalFunctor

MappingCone

Pretriangulated

Shift

ShiftSequence

ShortExact

SingleFunctors

Triangulated

ShortComplex

Ab

Abelian

Basic

ConcreteCategory

Exact

ExactFunctor

FunctorEquivalence

HomologicalComplex

Homology

LeftHomology

Limits

Linear

ModuleCat

Preadditive

PreservesHomology

QuasiIso

Retract

RightHomology

ShortExact

SnakeLemma

Additive

AlternatingConst

Augment

Bifunctor

BifunctorAssociator

BifunctorFlip

BifunctorHomotopy

BifunctorShift

CommSq

ComplexShape

ComplexShapeSigns

ConcreteCategory

DifferentialObject

Double

ExactSequence

Functor

GrothendieckAbelian

HasNoLoop

HomologicalBicomplex

HomologicalComplex

HomologicalComplexAbelian

HomologicalComplexBiprod

HomologicalComplexLimits

HomologySequence

HomologySequenceLemmas

Homotopy

HomotopyCofiber

ImageToKernel

Linear

LocalCohomology

Localization

Monoidal

Opposite

QuasiIso

Refinements

Single

SingleHomology

Square

TotalComplex

TotalComplexShift

TotalComplexSymmetry

Jordan

Basic

Lie

Derivation

AdjointAction

Basic

Killing

Semisimple

Basic

Defs

Lemmas

Weights

Basic

Cartan

Chain

Killing

Linear

RootSystem

Abelian

BaseChange

Basic

CartanExists

CartanMatrix

CartanSubalgebra

Character

Classical

DirectSum

Engel

EngelSubalgebra

Extension

Free

Ideal

IdealOperations

InvariantForm

Killing

LieTheorem

Matrix

Nilpotent

NonUnitalNonAssocAlgebra

Normalizer

OfAssociative

Quotient

Rank

SkewAdjoint

Sl2

Solvable

Subalgebra

Submodule

TensorProduct

TraceForm

UniversalEnveloping

Module

Equiv

Basic

Defs

Opposite

LinearMap

Basic

Defs

End

Polynomial

Prod

Rat

Star

LocalizedModule

AtPrime

Away

Basic

Exact

Int

IsLocalization

Submodule

Presentation

Basic

Cokernel

Differentials

DirectSum

Finite

Free

RestrictScalars

Tautological

Tensor

Submodule

Basic

Bilinear

Defs

EqLocus

Equiv

Invariant

IterateMapComap

Ker

Lattice

LinearMap

Map

Order

Pointwise

Range

RestrictScalars

ZLattice

Basic

Covolume

Basic

BigOperators

Bimodule

Card

CharacterModule

DedekindDomain

Defs

End

FinitePresentation

GradedModule

Hom

Injective

Lattice

MinimalAxioms

NatInt

Opposite

PID

PUnit

Pi

PointwisePi

Prod

Projective

Rat

RingHom

Shrink

SnakeLemma

SpanRank

Torsion

TransferInstance

ULift

ZMod

MonoidAlgebra

Basic

Defs

Degree

Division

Grading

Ideal

MapDomain

NoZeroDivisors

Support

ToDirectSum

MvPolynomial

Basic

Cardinal

Comap

CommRing

Counit

Degrees

Derivation

Division

Equiv

Eval

Expand

Funext

Invertible

Monad

Nilpotent

PDeriv

Polynomial

Rename

SchwartzZippel

Supported

Variables

NoZeroSMulDivisors

Basic

Defs

Pi

Prod

Notation (file)

Defs

Lemmas

Pi

Prod

Order

AbsoluteValue

Basic

Euclidean

Antidiag

Finsupp

Nat

Pi

Prod

Archimedean

Basic

Class

Hom

IndicatorCard

Submonoid

BigOperators

Group

Finset

List

LocallyFinite

Multiset

GroupWithZero

List

Multiset

Ring

Finset

List

Multiset

Expect

CauSeq

Basic

BigOperators

Completion

Field

Basic

Canonical

Defs

InjSurj

Pi

Pointwise

Power

Rat

Subfield

Floor (file)

Defs

Div

Ring

Semiring

Group

Action (file)

End

Flag

Synonym

Int (file)

Sum

Pointwise

Bounds

CompleteLattice

Interval

Unbundled

Abs

Basic

Int

Abs

Basic

Bounds

CompleteLattice

Cone

Cyclic

Defs

DenselyOrdered

End

Finset

Indicator

InjSurj

Instances

Lattice

MinMax

Multiset

Nat

Opposite

OrderIso

PiLex

PosPart

Prod

Synonym

TypeTags

Units

GroupWithZero

Action

Synonym

Unbundled (file)

Basic

Defs

Lemmas

OrderIso

Bounds

Canonical

Finset

Lex

Submonoid

Synonym

WithZero

Hom

Basic

Monoid

Ring

Interval

Finset

Basic

SuccPred

Set

Group

Instances

Monoid

SuccPred

Basic

Multiset

Module

Algebra

Basic

Defs

Field

OrderedSMul

Pointwise

PositiveLinearMap

Rat

Synonym

Monoid

Canonical

Basic

Defs

Unbundled

Basic

Defs

ExistsOfLE

MinMax

OrderDual

Pow

TypeTags

WithTop

Associated

Basic

Defs

Lex

NatCast

OrderDual

Prod

Submonoid

ToMulBot

TypeTags

Units

WithTop

Nonneg

Basic

Field

Floor

Lattice

Module

Ring

Positive

Field

Ring

Ring

Unbundled

Basic

Rat

Abs

Basic

Canonical

Cast

Cone

Defs

Finset

Idempotent

InjSurj

Int

IsNonarchimedean

Nat

Opposite

Pow

Prod

Rat

Star

Synonym

WithTop

Star

Basic

Conjneg

Prod

Sub

Unbundled

Basic

Hom

Basic

Defs

Prod

WithTop

SuccPred (file)

TypeTags

WithBot

WithTop

Untop0

AddGroupWithTop

AddTorsor

Algebra

Chebyshev

CompleteField

Disjointed

Invertible

Kleene

Monovary

PUnit

PartialSups

Pi

Quantale

Rearrangement

Round

Sum

ToIntervalMod

UpperLower

ZeroLEOne

Pointwise

Stabilizer

Polynomial

Degree

CardPowDegree

Definitions

Domain

IsMonicOfDegree

Lemmas

Monomial

Operations

SmallDegree

Support

TrailingDegree

Units

Eval

Algebra

Coeff

Defs

Degree

Irreducible

SMul

Subring

Module

AEval

Basic

FiniteDimensional

AlgebraMap

Basic

Basis

BigOperators

Bivariate

CancelLeads

Cardinal

Coeff

CoeffList

CoeffMem

DenomsClearable

Derivation

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Mirror

Monic

Monomial

OfFn

PartialFractions

Reverse

RingDivision

Roots

Sequence

Smeval

SpecificDegree

Splits

SumIteratedDerivative

Taylor

UnitTrinomial

PresentedMonoid

Basic

Prime

Defs

Lemmas

Regular

Basic

Opposite

Pi

Pow

Prod

SMul

ULift

Ring

Action

Pointwise

Finset

Set

Basic

ConjAct

End

Field

Group

Invariant

Rat

Submonoid

Subobjects

Divisibility

Basic

Lemmas

Hom

Basic

Defs

InjSurj

Int

Defs

Parity

Units

Pointwise

Finset

Set

Semireal

Defs

Submonoid (file)

Basic

Pointwise

Subring

Basic

Defs

IntPolynomial

MulOpposite

Order

Pointwise

Units

Subsemiring

Basic

Defs

MulOpposite

Order

Pointwise

AddAut

Associated

Associator

Aut

Basic

BooleanRing

Center

Centralizer

CentroidHom

CharZero

Commute

CompTypeclasses

Defs

Equiv

Ext

Fin

GrindInstances

Idempotent

Identities

InjSurj

Invertible

MinimalAxioms

Nat

NegOnePow

NonZeroDivisors

Opposite

PUnit

Parity

Periodic

Pi

Prod

Rat

Regular

Semiconj

Shrink

Subgroup

SumsOfSquares

TransferInstance

ULift

Units

WithZero

SkewMonoidAlgebra

Basic

Squarefree

Basic

Star

Basic

BigOperators

CHSH

Center

CentroidHom

Conjneg

Free

Module

NonUnitalSubalgebra

NonUnitalSubsemiring

Pi

Pointwise

Prod

Rat

RingQuot

SelfAdjoint

StarAlgHom

StarProjection

StarRingHom

Subalgebra

Subsemiring

Unitary

Tropical

Basic

BigOperators

Lattice

Vertex

HVertexOperator

VertexOperator

AlgebraicCard

CubicDiscriminant

DualNumber

DualQuaternion

Exact

Expr

FiveLemma

Free

FreeNonUnitalNonAssocAlgebra

GeomSum

GradedMonoid

GradedMulAction

HierarchyDesign

IsPrimePow

LinearRecurrence

ModEq

NeZero

Opposites

PEmptyInstances

QuadraticDiscriminant

Quandle

Quaternion

QuaternionBasis

Quotient

RingQuot

Symmetrized

TrivSqZeroExt

AlgebraicGeometry

Cover

MorphismProperty

Open

Over

Sigma

EllipticCurve

Affine (file)

Basic

Formula

Point

DivisionPolynomial

Basic

Degree

Jacobian

Basic

Formula

Point

Projective

Basic

Formula

Point

Group

IsomOfJ

ModelsWithJ

NormalForms

VariableChange

Weierstrass

IdealSheaf (file)

Basic

Functorial

Subscheme

Modules

Presheaf

Sheaf

Tilde

Morphisms

Affine

AffineAnd

Basic

ClosedImmersion

Constructors

Etale

Finite

FinitePresentation

FiniteType

Flat

FormallyUnramified

Immersion

Integral

IsIso

OpenImmersion

Preimmersion

Proper

QuasiCompact

QuasiSeparated

RingHomProperties

Separated

Smooth

SurjectiveOnStalks

UnderlyingMap

UniversallyClosed

UniversallyInjective

UniversallyOpen

ProjectiveSpectrum

Basic

Proper

Scheme

StructureSheaf

Topology

Sites

BigZariski

Etale

MorphismProperty

Representability

Small

SmallAffineZariski

AffineScheme

AffineSpace

AffineTransitionLimit

Fiber

FunctionField

GammaSpecAdjunction

Gluing

GluingOneHypercover

Limits

Noetherian

OpenImmersion

Over

PointsPi

Properties

PullbackCarrier

Pullbacks

RationalMap

ResidueField

Restrict

Scheme

Spec

SpreadingOut

Stalk

StructureSheaf

ValuativeCriterion

AlgebraicTopology

DoldKan

Compatibility

Decomposition

Degeneracies

Equivalence

EquivalenceAdditive

EquivalencePseudoabelian

Faces

FunctorGamma

FunctorN

GammaCompN

Homotopies

HomotopyEquivalence

NCompGamma

NReflectsIso

Normalized

Notations

PInfty

Projections

SplitSimplicialObject

FundamentalGroupoid

Basic

FundamentalGroup

InducedMaps

PUnit

Product

SimplyConnected

ModelCategory

Basic

CategoryWithCofibrations

Cylinder

Instances

IsCofibrant

Quasicategory

Basic

Nerve

StrictSegal

RelativeCellComplex

AttachCells

Basic

SimplexCategory

GeneratorsRelations

Basic

EpiMono

NormalForms

Augmented

Basic

Defs

MorphismProperty

Truncated

SimplicialCategory

Basic

SimplicialObject

SimplicialObject

Basic

Coskeletal

Split

SimplicialSet

Basic

Boundary

CategoryWithFibrations

Coskeletal

Degenerate

HomotopyCat

Horn

KanComplex

Monoidal

Nerve

NerveAdjunction

Path

StdSimplex

StrictSegal

Subcomplex

SingularHomology

Basic

AlternatingFaceMapComplex

CechNerve

ExtraDegeneracy

MooreComplex

SimplicialNerve

SingularSet

TopologicalSimplex

Analysis

AbsoluteValue

Equivalence

Analytic

Basic

CPolynomial

CPolynomialDef

ChangeOrigin

Composition

Constructions

Inverse

IsolatedZeros

IteratedFDeriv

Linear

OfScalars

Order

Polynomial

RadiusLiminf

Uniqueness

Within

Asymptotics

AsymptoticEquivalent

Completion

Defs

ExpGrowth

Lemmas

LinearGrowth

SpecificAsymptotics

SuperpolynomialDecay

TVS

Theta

BoxIntegral

Box

Basic

SubboxInduction

Partition

Additive

Basic

Filter

Measure

Split

SubboxInduction

Tagged

Basic

DivergenceTheorem

Integrability

UnitPartition

CStarAlgebra

ContinuousFunctionalCalculus

Basic

Continuity

Instances

Integral

Isometric

NonUnital

Note

Order

Pi

Restrict

Unique

Unital

Unitary

Module

Constructions

Defs

Synonym

SpecialFunctions

PosPart

ApproximateUnit

Basic

CStarMatrix

Classes

CompletelyPositiveMap

ContinuousLinearMap

ContinuousMap

Exponential

GelfandDuality

Hom

Matrix

Multiplier

PositiveLinearMap

Spectrum

Unitization

lpSpace

Calculus

AddTorsor

AffineMap

Coord

BumpFunction

Basic

Convolution

FiniteDimension

InnerProduct

Normed

SmoothApprox

Conformal

InnerProduct

NormedSpace

ContDiff

Basic

Bounds

CPolynomial

Defs

FTaylorSeries

FaaDiBruno

FiniteDimension

Operations

RCLike

RestrictScalars

WithLp

Deriv

Abs

Add

AffineMap

Basic

Comp

CompMul

Inv

Inverse

Linear

MeanValue

Mul

Pi

Polynomial

Pow

Prod

Shift

Slope

Star

Support

ZPow

FDeriv

Add

Analytic

Basic

Bilinear

Comp

Congr

Const

Defs

Equiv

Extend

Linear

Measurable

Mul

Norm

Pi

Pow

Prod

RestrictScalars

Star

Symmetric

WithLp

Gradient

Basic

InverseFunctionTheorem

ApproximatesLinearOn

ContDiff

Deriv

FDeriv

FiniteDimensional

IteratedDeriv

Defs

FaaDiBruno

Lemmas

WithinZpow

LineDeriv

Basic

IntegrationByParts

Measurable

QuadraticMap

LocalExtr

Basic

LineDeriv

Polynomial

Rolle

DSlope

Darboux

DerivativeTest

DiffContOnCl

FormalMultilinearSeries

Implicit

LHopital

LagrangeMultipliers

LogDeriv

MeanValue

Monotone

ParametricIntegral

ParametricIntervalIntegral

Rademacher

SmoothSeries

TangentCone

Taylor

UniformLimitsDeriv

VectorField

Complex

Polynomial

Basic

UnitTrinomial

UnitDisc

Basic

UpperHalfPlane

Basic

Exp

FunctionsBoundedAtInfty

Manifold

Metric

MoebiusAction

Topology

ValueDistribution

CharacteristicFunction

CountingFunction

FirstMainTheorem

ProximityFunction

AbelLimit

AbsMax

Angle

Arg

Asymptotics

Basic

CauchyIntegral

Circle

Conformal

Convex

Hadamard

HalfPlane

IntegerCompl

IsIntegral

Isometry

Liouville

LocallyUniformLimit

OpenMapping

OperatorNorm

Periodic

PhragmenLindelof

Positivity

ReImTopology

RealDeriv

RemovableSingularity

Schwarz

TaylorSeries

Tietze

Convex

Cone

Basic

Closure

Dual

Extension

InnerDual

SimplicialComplex

Basic

SpecificFunctions

Basic

Deriv

Pow

AmpleSet

Basic

Between

BetweenList

Birkhoff

Body

Caratheodory

Combination

Continuous

Contractible

Deriv

EGauge

Exposed

Extrema

Extreme

Function

Gauge

GaugeRescale

Hull

Independent

Integral

Intrinsic

Jensen

Join

KreinMilman

Measure

Mul

PartitionOfUnity

PathConnected

Piecewise

Quasiconvex

Radon

Segment

Side

Slope

Star

StoneSeparation

Strict

StrictConvexBetween

StrictConvexSpace

Strong

Topology

TotallyBounded

Uniform

Visible

Distribution

AEEqOfIntegralContDiff

FourierSchwartz

SchwartzSpace

Fourier

FiniteAbelian

Orthogonality

PontryaginDuality

AddCircle

AddCircleMulti

BoundedContinuousFunctionChar

FourierTransform

FourierTransformDeriv

Inversion

PoissonSummation

RiemannLebesgueLemma

ZMod

FunctionalSpaces

SobolevInequality

InnerProductSpace

Harmonic

Basic

Adjoint

Affine

Basic

Calculus

CanonicalTensor

Completion

ConformalLinearMap

Continuous

Convex

Defs

Dual

EuclideanDist

GramSchmidtOrtho

JointEigenspace

Laplacian

LaxMilgram

LinearMap

LinearPMap

MeanErgodic

NormPow

OfNorm

Orientation

Orthogonal

Orthonormal

PiL2

Positive

ProdL2

Projection

Rayleigh

Semisimple

Spectrum

StarOrder

Subspace

Symmetric

Trace

TwoDim

WeakOperatorTopology

l2Space

LocallyConvex

AbsConvex

AbsConvexOpen

BalancedCoreHull

Barrelled

Basic

Bounded

ContinuousOfBounded

Polar

StrongTopology

WeakDual

WeakOperatorTopology

WeakSpace

WithSeminorms

Meromorphic

Basic

Divisor

FactorizedRational

Gamma

IsolatedZeros

NormalForm

Order

TrailingCoefficient

Normed

Affine

AddTorsor

AddTorsorBases

ContinuousAffineMap

Convex

Isometry

MazurUlam

Simplex

Algebra

Basic

Exponential

MatrixExponential

QuaternionExponential

Spectrum

TrivSqZeroExt

Ultra

Unitization

UnitizationL1

Field

Basic

Instances

Lemmas

ProperSpace

Ultra

UnitBall

WithAbs

Group

SemiNormedGrp (file)

Completion

Kernels

AddCircle

AddTorsor

BallSphere

Basic

Bounded

CocompactMap

Completeness

Completion

Constructions

Continuity

ControlledClosure

Hom

HomCompletion

InfiniteSum

Int

Lemmas

NullSubmodule

Pointwise

Quotient

Rat

Seminorm

SeparationQuotient

Subgroup

Submodule

Tannery

Ultra

Uniform

ZeroAtInfty

Lp

LpEquiv

MeasurableSpace

PiLp

ProdLp

WithLp

lpSpace

Module

Basic

Complemented

Completion

Convex

Dual

FiniteDimension

Ray

Span

WeakDual

Operator

Banach

BanachSteinhaus

BoundedLinearMaps

Compact

ContinuousLinearMap

LinearIsometry

Order

Hom

Basic

Ultra

Basic

Lattice

UpperLower

Ring

Basic

InfiniteSum

Lemmas

Ultra

Units

WithAbs

Unbundled

AlgebraNorm

FiniteExtension

InvariantExtension

IsPowMulFaithful

RingSeminorm

SeminormFromBounded

SeminormFromConst

SmoothingSeminorm

SpectralNorm

MulAction

NormedSpace

Alternating

Basic

Curry

HahnBanach

Extension

SeparatingDual

Separation

Multilinear

Basic

Curry

OperatorNorm

Asymptotics

Basic

Bilinear

Completeness

Mul

NNNorm

NormedSpace

Prod

PiTensorProduct

InjectiveSeminorm

ProjectiveSeminorm

BallAction

ConformalLinearMap

Connected

DualNumber

ENormedSpace

Extend

Extr

FunctionSeries

HomeomorphBall

IndicatorFunction

Int

MStructure

MultipliableUniformlyOn

Pointwise

RCLike

Real

RieszLemma

SphereNormEquiv

ODE

Gronwall

PicardLindelof

Polynomial

Basic

CauchyBound

RCLike

Basic

BoundedContinuous

Inner

Lemmas

TangentCone

SpecialFunctions

Complex

Analytic

Arctan

Arg

Circle

CircleAddChar

CircleMap

Log

LogBounds

LogDeriv

ContinuousFunctionalCalculus

PosPart

Basic

Isometric

Rpow

Basic

IntegralRepresentation

Isometric

ExpLog

Gamma

Basic

Beta

BohrMollerup

Deligne

Deriv

Gaussian

FourierTransform

GaussianIntegral

PoissonSummation

Integrability

Basic

LogMeromorphic

Integrals

Basic

LogTrigonometric

Log

Base

Basic

Deriv

ENNRealLog

ENNRealLogExp

ERealExp

Monotone

NegMulLog

PosLog

Summable

Pow

Asymptotics

Complex

Continuity

Deriv

Integral

NNReal

Real

Trigonometric

Angle

Arctan

ArctanDeriv

Basic

Bounds

Chebyshev

Complex

ComplexDeriv

Cotangent

Deriv

EulerSineProd

Inverse

InverseDeriv

Series

Sinc

Arsinh

Bernstein

BinaryEntropy

Choose

CompareExp

Exp

ExpDeriv

Exponential

ImproperIntegrals

JapaneseBracket

MulExpNegMulSq

MulExpNegMulSqIntegral

NonIntegrable

OrdinaryHypergeometric

Pochhammer

PolarCoord

PolynomialExp

SmoothTransition

Sqrt

Stirling

SpecificLimits

Basic

FloorPow

Normed

RCLike

VonNeumannAlgebra

Basic

BoundedVariation

ConstantSpeed

Convolution

Hofer

LConvolution

Matrix

MeanInequalities

MeanInequalitiesPow

MellinInversion

MellinTransform

Oscillation

PSeries

PSeriesComplex

Quaternion

Seminorm

Subadditive

SumIntegralComparisons

SumOverResidueClass

CategoryTheory

Abelian

DiagramLemmas

Four

KernelCokernelComp

GrothendieckAxioms

Basic

Colim

Connected

FunctorCategory

Indization

Sheaf

Types

GrothendieckCategory

ModuleEmbedding

GabrielPopescu

Opposite

Basic

ColimCoyoneda

Coseparator

EnoughInjectives

Monomorphisms

Subobject

Injective

Basic

Resolution

Projective

Basic

Dimension

Resolution

SerreClass

Basic

MorphismProperty

Basic

CommSq

EpiWithInjectiveKernel

Exact

Ext

FreydMitchell

FunctorCategory

Images

Indization

LeftDerived

Monomorphisms

NonPreadditive

Opposite

Pseudoelements

Refinements

RightDerived

Subobject

Transfer

Yoneda

Action (file)

Basic

Concrete

Continuous

Limits

Monoidal

Adjunction

Lifting

Left

Right

Additive

AdjointFunctorTheorems

Basic

Comma

Evaluation

FullyFaithful

Limits

Mates

Opposites

Parametrized

PartialAdjoint

Reflective

Restrict

Triple

Unique

Whiskering

Bicategory

Adjunction

Adj

Basic

Mate

Functor

Lax

LocallyDiscrete

Oplax

Prelax

Pseudofunctor

Strict

FunctorBicategory

Oplax

Kan

Adjunction

HasKan

IsKan

Modification

Oplax

Monad

Basic

NaturalTransformation

Oplax

Pseudo

Strong

Basic

CatEnriched

Coherence

End

Extension

Free

Grothendieck

LocallyDiscrete

SingleObj

Strict

Category

Cat (file)

Adjunction

AsSmall

CartesianClosed

Colimit

Limit

Op

Terminal

Basic

Bipointed

Factorisation

GaloisConnection

Grpd

Init

KleisliCat

Pairwise

PartialFun

Pointed

Preorder

Quiv

ReflQuiv

RelCat

TwoP

ULift

Center

Basic

Linear

Localization

ChosenFiniteProducts (file)

Cat

FunctorCategory

InfSemilattice

Over

Closed

FunctorCategory

Basic

Complete

Groupoid

Cartesian

Enrichment

Functor

FunctorToTypes

Ideal

Monoidal

Types

Zero

Comma

Over

Basic

OverClass

Pullback

Presheaf

Basic

Colimit

StructuredArrow

Basic

CommaMap

Final

Functor

Small

Arrow

Basic

CardinalArrow

Final

LocallySmall

ConcreteCategory

Basic

Bundled

BundledHom

Elementwise

EpiMono

ReflectsIso

UnbundledHom

Dialectica

Basic

Monoidal

Discrete

Basic

SumsProducts

Distributive

Cartesian

Monoidal

EffectiveEpi

Basic

Comp

Coproduct

Enough

Extensive

Preserves

RegularEpi

Endofunctor

Algebra

Enriched

Limits

HasConicalLimits

HasConicalProducts

HasConicalPullbacks

HasConicalTerminal

Ordinary

Basic

Basic

FunctorCategory

HomCongr

Opposite

Equivalence (file)

Symmetry

FiberedCategory

BasedCategory

Cartesian

Cocartesian

Fiber

Fibered

Grothendieck

HasFibers

HomLift

Filtered

Basic

Connected

CostructuredArrow

Final

Flat

Grothendieck

OfColimitCommutesFiniteLimit

Small

FinCategory

AsType

Basic

Functor

Derived

Adjunction

LeftDerived

RightDerived

KanExtension

Adjunction

Basic

Pointwise

Preserves

ReflectsIso

Balanced

Basic

Basic

Category

Const

Currying

CurryingThree

EpiMono

Flat

FullyFaithful

FunctorHom

Functorial

Hom

OfSequence

Trifunctor

TwoSquare

Galois

Action

Basic

Decomposition

Equivalence

EssSurj

Examples

Full

GaloisObjects

IsFundamentalgroup

Prorepresentability

Topology

Generator

Abelian

Basic

HomologicalComplex

Indization

Preadditive

Presheaf

Sheaf

GradedObject (file)

Associator

Bifunctor

Braiding

Monoidal

Single

Trifunctor

Unitor

Groupoid (file)

Basic

Discrete

FreeGroupoid

Subgroupoid

VertexGroup

GuitartExact

Basic

Opposite

VerticalComposition

Idempotents

Basic

Biproducts

FunctorCategories

FunctorExtension

HomologicalComplex

Karoubi

KaroubiKaroubi

SimplicialObject

Join

Basic

Final

Opposites

Pseudofunctor

Sum

LiftingProperties

Adjunction

Basic

Limits

ParametrizedAdjunction

Limits

ConcreteCategory

Basic

WithAlgebraicStructures

Constructions

Over

Basic

Connected

Products

BinaryProducts

EpiMono

Equalizers

EventuallyConstant

Filtered

FiniteProductsOfBinaryProducts

LimitsOfProductsAndEqualizers

Pullbacks

WeaklyInitial

ZeroObjects

Final (file)

ParallelPair

FunctorCategory

Shapes

Products

Pullbacks

Basic

EpiMono

Filtered

Finite

Indization

Category

Equalizers

FilteredColimits

IndObject

LocallySmall

ParallelPair

Products

Preserves

Creates

Finite

Shapes

AbelianImages

BinaryProducts

Biproducts

Equalizers

Images

Kernels

Multiequalizer

Preorder

Products

Pullbacks

Square

Terminal

Zero

Basic

Bifunctor

Filtered

Finite

FunctorCategory

Grothendieck

Limits

Opposites

Over

Presheaf

Ulift

Yoneda

Shapes

NormalMono

Basic

Equalizers

Preorder

Basic

Fin

HasIterationOfShape

PrincipalSeg

TransfiniteCompositionOfShape

WellOrderContinuous

Pullback

Categorical

Basic

CatCospanTransform

Assoc

CommSq

Cospan

Equalizer

HasPullback

Iso

Mono

Pasting

PullbackCone

Square

BinaryBiproducts

BinaryProducts

Biproducts

CombinedProducts

ConcreteCategory

Connected

Countable

Diagonal

DisjointCoproduct

End

Equalizers

Equivalence

FiniteLimits

FiniteMultiequalizer

FiniteProducts

FunctorToTypes

Grothendieck

Images

IsTerminal

KernelPair

Kernels

Multiequalizer

MultiequalizerPullback

PiProd

Products

Reflexive

RegularMono

SequentialProduct

SingleObj

SplitCoequalizer

SplitEqualizer

StrictInitial

StrongEpi

Terminal

WideEqualizers

WidePullbacks

ZeroMorphisms

ZeroObjects

Types

ColimitType

Colimits

Filtered

Images

Limits

Shapes

Yoneda

Bicones

ColimitLimit

Comma

ConeCategory

Cones

Connected

Creates

Elements

EpiMono

EssentiallySmall

ExactFunctor

Filtered

FilteredColimitCommutesFiniteLimit

FilteredColimitCommutesProduct

FinallySmall

FintypeCat

FormalCoproducts

Fubini

FullSubcategory

FunctorToTypes

HasLimits

IndYoneda

IsConnected

IsLimit

Lattice

MonoCoprod

MorphismProperty

Opposites

Over

Pi

Preorder

Presheaf

Set

Sifted

SmallComplete

Unit

VanKampen

Yoneda

Linear

Basic

FunctorCategory

LinearFunctor

Yoneda

Localization

CalculusOfFractions (file)

ComposableArrows

Fractions

OfAdjunction

Preadditive

DerivabilityStructure

Basic

Constructor

OfFunctorialResolutions

Adjunction

Bifunctor

Bousfield

Composition

Construction

Equivalence

FiniteProducts

HasLocalization

HomEquiv

Linear

LocalizerMorphism

LocallySmall

Monoidal

Opposite

Pi

Preadditive

Predicate

Prod

Resolution

SmallHom

SmallShiftedHom

StructuredArrow

Triangulated

Trifunctor

Monad

Adjunction

Algebra

Basic

Coequalizer

Comonadicity

Equalizer

EquivMon

Kleisli

Limits

Monadicity

Products

Types

Monoidal

Action

Basic

LinearFunctor

Opposites

Braided

Basic

Opposite

Reflection

Cartesian

Basic

Cat

CommGrp_

CommMon_

Comon_

FunctorCategory

Grp_

InfSemilattice

Mod_

Mon_

Over

ExternalProduct (file)

Basic

KanExtension

Free

Basic

Coherence

Internal

Types

Basic

CommGrp_

Grp_

FunctorCategory

Limits

Module

OfChosenFiniteProducts

Basic

Symmetric

Rigid

Basic

Braided

FunctorCategory

OfEquivalence

Types

Basic

Coyoneda

Bimod

Bimon_

Category

Center

CoherenceLemmas

CommGrp_

CommMon_

Comon_

Conv

DayConvolution

Discrete

End

Functor

FunctorCategory

Grp_

Hopf_

Limits

Linear

Mod_

Mon_

NaturalTransformation

OfHasFiniteProducts

Opposite

Preadditive

Skeleton

Subcategory

Tor

Transport

Yoneda

MorphismProperty

Basic

Comma

Composition

Concrete

Descent

Factorization

FunctorCategory

IsInvertedBy

IsSmall

LiftingProperty

Limits

OverAdjunction

Representable

Retract

RetractArgument

TransfiniteComposition

WeakFactorizationSystem

ObjectProperty

Basic

ClosedUnderIsomorphisms

ContainsZero

EpiMono

Extensions

FullSubcategory

Shift

PathCategory

Basic

MorphismProperty

Pi

Basic

Preadditive

Injective

Basic

LiftingProperties

Preserves

Resolution

Projective

Basic

LiftingProperties

Preserves

Resolution

Yoneda

Basic

Injective

Limits

Projective

AdditiveFunctor

Basic

Biproducts

CommGrp_

EilenbergMoore

EndoFunctor

FunctorCategory

HomOrthogonal

Indization

LeftExact

LiftToFinset

Mat

OfBiproducts

Opposite

Schur

SingleObj

Transfer

Presentable

Basic

Finite

IsCardinalFiltered

Limits

Products

Associator

Basic

Bifunctor

Unitor

Quotient (file)

Linear

Preadditive

Shift

Adjunction

Basic

CommShift

Induced

InducedShiftSequence

Linear

Localization

Opposite

Pullback

Quotient

ShiftSequence

ShiftedHom

ShiftedHomOpposite

SingleFunctors

Sigma

Basic

Sites

Coherent

Basic

CoherentSheaves

CoherentTopology

Comparison

Equivalence

ExtensiveColimits

ExtensiveSheaves

ExtensiveTopology

LocallySurjective

ReflectsPrecoherent

ReflectsPreregular

RegularSheaves

RegularTopology

SequentialLimit

SheafComparison

DenseSubsite

Basic

InducedTopology

SheafEquiv

NonabelianCohomology

H1

SheafCohomology

Basic

Abelian

Adjunction

Canonical

CartesianClosed

CartesianMonoidal

ChosenFiniteProducts

Closed

CompatiblePlus

CompatibleSheafification

ConcreteSheafification

ConstantSheaf

Continuous

CoverLifting

CoverPreserving

Coverage

CoversTop

EffectiveEpimorphic

EpiMono

EqualizerSheafCondition

Equivalence

GlobalSections

Grothendieck

IsSheafFor

IsSheafOneHypercover

LeftExact

Limits

Localization

LocallyBijective

LocallyFullyFaithful

LocallyInjective

LocallySurjective

MayerVietorisSquare

Monoidal

MorphismProperty

OneHypercover

Over

Plus

Preserves

PreservesLocallyBijective

PreservesSheafification

Pretopology

Pullback

Sheaf

SheafHom

SheafOfTypes

Sheafification

Sieves

Spaces

Subcanonical

Subsheaf

Types

Whiskering

ZeroHypercover

SmallObject

Iteration

Basic

ExtendToSucc

FunctorOfCocone

Nonempty

Basic

Construction

IsCardinalForSmallObjectArgument

TransfiniteCompositionLifting

TransfiniteIteration

WellOrderInductionData

Subobject

Basic

Comma

FactorThru

HasCardinalLT

Lattice

Limits

MonoOver

NoetherianObject

Presheaf

Types

WellPowered

Subpresheaf

Basic

Equalizer

Finite

Image

OfSection

Sieves

Subobject

Sums

Associator

Basic

Products

Topos

Classifier

Triangulated

Opposite

Basic

Functor

Pretriangulated

Triangle

TStructure

Basic

Adjunction

Basic

Functor

HomologicalFunctor

Pretriangulated

Rotate

Subcategory

TriangleShift

Triangulated

Yoneda

WithTerminal (file)

Basic

Cone

FinCategory

Adhesive

Balanced

CatCommSq

CodiscreteCategory

CofilteredSystem

CommSq

ComposableArrows

Conj

ConnectedComponents

Core

Countable

DifferentialObject

DinatTrans

Elements

Elementwise

Endomorphism

EpiMono

EqToHom

EssentialImage

EssentiallySmall

Extensive

FintypeCat

FullSubcategory

GlueData

Grothendieck

HomCongr

InducedCategory

IsConnected

Iso

IsomorphismClasses

LocallyDirected

NatIso

NatTrans

Noetherian

Opposites

PEmpty

PUnit

Retract

Simple

SingleObj

Skeletal

Square

Subterminal

Thin

Types

UnivLE

Whiskering

Widesubcategory

Yoneda

Combinatorics

Additive

AP

Three

Behrend

Defs

Corner

Defs

Roth

ApproximateSubgroup

CauchyDavenport

CovBySMul

Dissociation

DoublingConst

ETransform

Energy

ErdosGinzburgZiv

FreimanHom

PluenneckeRuzsa

Randomisation

RuzsaCovering

SmallTripling

VerySmallDoubling

Derangements

Basic

Exponential

Finite

Digraph

Basic

Orientation

Enumerative

Bell

Catalan

Composition

DoubleCounting

DyckWord

IncidenceAlgebra

InclusionExclusion

Partition

Extremal

RuzsaSzemeredi

Graph

Basic

Hall

Basic

Finite

Optimization

ValuedCSP

Quiver

Arborescence

Basic

Cast

ConnectedComponent

Covering

Path

Prefunctor

Push

ReflQuiver

SingleObj

Subquiver

Symmetric

SetFamily

Compression

Down

UV

AhlswedeZhang

FourFunctions

HarrisKleitman

Intersecting

Kleitman

KruskalKatona

LYM

Shadow

Shatter

SimpleGraph

Connectivity

Connected

Represents

Subgraph

WalkCounting

WalkDecomp

Ends

Defs

Properties

Extremal

Basic

Regularity

Bound

Chunk

Energy

Equitabilise

Increment

Lemma

Uniform

Triangle

Basic

Counting

Removal

Tripartite

Acyclic

AdjMatrix

Basic

Bipartite

Circulant

Clique

Coloring

CompleteMultipartite

ConcreteColorings

Copy

Dart

DegreeSum

DeleteEdges

Density

Diam

Finite

Finsubgraph

FiveWheelLike

Girth

Hamiltonian

Hasse

IncMatrix

Init

LapMatrix

LineGraph

Maps

Matching

Metric

Operations

Partition

Path

Paths

Prod

StronglyRegular

Subgraph

Sum

Trails

Turan

Tutte

UniversalVerts

Walk

Young

SemistandardTableau

YoungDiagram

Colex

Configuration

HalesJewett

Hindman

Nullstellensatz

Pigeonhole

Schnirelmann

Computability

AkraBazzi

AkraBazzi

GrowsPolynomially

SumTransform

Ackermann

ContextFreeGrammar

DFA

Encoding

EpsilonNFA

Halting

Language

MyhillNerode

NFA

Partrec

PartrecCode

PostTuringMachine

Primrec

Reduce

RegularExpressions

TMComputable

TMConfig

TMToPartrec

Tape

TuringDegree

TuringMachine

Condensed

Discrete

Basic

Characterization

Colimit

LocallyConstant

Module

Light

AB

Basic

CartesianClosed

Epi

Explicit

Functors

Limits

Module

TopCatAdjunction

TopComparison

AB

Basic

CartesianClosed

Epi

Equivalence

Explicit

Functors

Limits

Module

Solid

TopCatAdjunction

TopComparison

Control

Bitraversable

Basic

Instances

Lemmas

EquivFunctor (file)

Instances

Functor (file)

Multivariate

Monad

Basic

Cont

Writer

Traversable

Basic

Equiv

Instances

Lemmas

Applicative

Basic

Bifunctor

Combinators

Fix

Fold

Lawful

LawfulFix

Random

ULift

ULiftable

Data

Analysis

Filter

Topology

Array

Defs

Extract

Bool

AllAny

Basic

Count

Set

Complex

Basic

BigOperators

Cardinality

Determinant

Exponential

ExponentialBounds

FiniteDimensional

Module

Norm

Order

Orientation

Trigonometric

Countable

Basic

Defs

Small

DFinsupp

BigOperators

Defs

Encodable

Ext

FiniteInfinite

Interval

Lex

Module

Multiset

NeLocus

Notation

Order

Sigma

Small

Submonoid

WellFounded

DList

Instances

ENNReal

Action

Basic

BigOperators

Holder

Inv

Lemmas

Operations

Order

Real

ENat

Basic

BigOperators

Defs

Lattice

EReal

Basic

Inv

Operations

FP

Basic

Fin

Tuple

Basic

BubbleSortInduction

Curry

Embedding

Finset

NatAntidiagonal

Reflection

Sort

Take

Basic

Embedding

Fin2

FlagRange

Parity

Pigeonhole

Rev

SuccPred

VecNotation

FinEnum (file)

Option

Finite

Card

Defs

Perm

Prod

Set

Sigma

Sum

Vector

Finset

Lattice

Basic

Fold

Lemmas

Pi

Prod

Union

Attach

Attr

Basic

BooleanAlgebra

Card

CastCard

Dedup

Defs

Density

Disjoint

Empty

Erase

Filter

Fin

Finsupp

Fold

Functor

Grade

Image

Insert

Interval

Max

MulAntidiagonal

NAry

NatAntidiagonal

NatDivisors

NoncommProd

Option

Order

PImage

Pairwise

Pi

PiInduction

Piecewise

Powerset

Preimage

Prod

Range

SDiff

SMulAntidiagonal

Sigma

Slice

Sort

Sum

Sups

Sym

SymmDiff

Union

Update

Finsupp

MonomialOrder (file)

DegLex

AList

Antidiagonal

Basic

BigOperators

Defs

Encodable

Ext

Fin

Fintype

Indicator

Interval

Lex

Multiset

NeLocus

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

Units

Vector

FunLike

Basic

Embedding

Equiv

Fintype

Int

Cast

Basic

Defs

Field

Lemmas

Pi

Prod

Order

Basic

Lemmas

Units

AbsoluteValue

Associated

Basic

Bitwise

CardIntervalMod

CharZero

ConditionallyCompleteOrder

DivMod

GCD

Init

Interval

LeastGreatest

Lemmas

Log

ModEq

NatAbs

NatPrime

Notation

Range

Sqrt

Star

SuccPred

WithZero

List

EditDistance

Bounds

Defs

Estimator

Perm

Basic

Lattice

Subperm

AList

Basic

Chain

ChainOfFn

Count

Cycle

Dedup

Defs

Destutter

DropRight

Duplicate

Enum

FinRange

Flatten

Forall2

GetD

Indexes

Induction

Infix

InsertIdx

InsertNth

Intervals

Iterate

Lattice

Lemmas

Lex

Lookmap

Map2

MinMax

ModifyLast

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

Pairwise

Palindrome

Permutation

Pi

Prime

ProdSigma

Range

ReduceOption

Rotate

Scan

Sections

Shortlex

Sigma

Sort

SplitBy

SplitLengths

SplitOn

Sublists

Sym

TFAE

TakeDrop

TakeWhile

ToFinsupp

Triplewise

Zip

MLList

BestFirst

Matrix

Auto

Basic

Basis

Bilinear

Block

CharP

ColumnRowPartitioned

Composition

ConjTranspose

DMatrix

Defs

Diagonal

DoublyStochastic

DualNumber

Hadamard

Invertible

Kronecker

Mul

Notation

PEquiv

Rank

Reflection

RowCol

Vec

Matroid

Minor

Contract

Delete

Order

Restrict

Rank

Cardinal

ENat

Finite

Basic

Circuit

Closure

Constructions

Dual

IndepAxioms

Init

Loop

Map

Sum

Multiset

AddSub

Antidiagonal

Basic

Bind

Count

Dedup

Defs

DershowitzManna

Filter

FinsetOps

Fintype

Fold

Functor

Interval

Lattice

MapFold

NatAntidiagonal

OrderedMonoid

Pairwise

Pi

Powerset

Range

Replicate

Sections

Sort

Sum

Sym

UnionInter

ZeroCons

NNRat

BigOperators

Defs

Floor

Lemmas

Order

NNReal

Basic

Defs

Star

Nat

Cast

Order

Basic

Field

Ring

Basic

Commute

Defs

Field

NeZero

Prod

SetInterval

Synonym

WithTop

Choose

Basic

Bounds

Cast

Central

Dvd

Factorization

Lucas

Mul

Multinomial

Sum

Vandermonde

Digits

Defs

Div

Lemmas

Factorial

Basic

BigOperators

Cast

DoubleFactorial

NatCast

SuperFactorial

Factorization

Basic

Defs

Induction

LCM

PrimePow

Root

Fib

Basic

Zeckendorf

GCD

Basic

BigOperators

Order

Lemmas

Prime

Basic

Defs

Factorial

Infinite

Int

Nth

Pow

Basic

BinaryRec

BitIndices

Bits

Bitwise

ChineseRemainder

Count

Dist

EvenOddRec

Factors

Find

Hyperoperation

Init

Lattice

Log

MaxPowDiv

ModEq

Multiplicity

Notation

Nth

PSub

Pairing

PartENat

Periodic

PrimeFin

Set

Size

Sqrt

Squarefree

SuccPred

Totient

Upto

WithBot

Num

Basic

Bitwise

Lemmas

Prime

ZNum

Option

Basic

Defs

NAry

Ordering

Basic

Lemmas

Ordmap

Invariants

Ordnode

Ordset

PFunctor

Multivariate

Basic

M

W

Univariate

Basic

M

PNat

Basic

Defs

Equiv

Factors

Find

Interval

Notation

Prime

Xgcd

PSigma

Order

Pi

Interval

Prod

Basic

Lex

PProd

TProd

QPF

Multivariate

Constructions

Cofix

Comp

Const

Fix

Prj

Quot

Sigma

Basic

Univariate

Basic

Rat

Cast

CharZero

Defs

Lemmas

Order

BigOperators

Cardinal

Defs

Denumerable

Encodable

Floor

Init

Lemmas

Sqrt

Star

Real

Pi

Bounds

Irrational

Leibniz

Wallis

Archimedean

Basic

Cardinality

CompleteField

ConjExponents

ENatENNReal

EReal

GoldenRatio

Hyperreal

Irrational

Pointwise

Sign

Sqrt

Star

StarOrdered

Seq

Computation

Parallel

Seq

WSeq

Set

Card (file)

Arithmetic

Finite

Basic

Lattice

Lemmas

List

Monad

Powerset

Range

Lattice (file)

Image

Pairwise

Basic

Lattice

List

Pointwise

Support

Accumulate

Basic

BoolIndicator

BooleanAlgebra

CoeSort

Constructions

Countable

Defs

Disjoint

Enumerate

Equitable

Function

Functor

FunctorToTypes

Image

Inclusion

Insert

List

MemPartition

Monotone

MulAntidiagonal

NAry

Notation

Operations

Opposite

Order

Piecewise

Prod

Restrict

SMulAntidiagonal

Semiring

Sigma

Subset

Subsingleton

Sups

SymmDiff

UnionLift

SetLike

Basic

Fintype

Setoid

Partition (file)

Card

Basic

Sigma

Basic

Interval

Lex

Order

Stream

Defs

Init

String

Basic

Defs

Lemmas

Sum

Basic

Interval

Lattice

Order

Sym

Sym2 (file)

Finsupp

Init

Order

Basic

Card

Tree

Basic

Get

RBMap

Traversable

Vector

Basic

Defs

MapLemmas

Mem

Snoc

Zip

W

Basic

Cardinal

Constructions

WSeq

Basic

Defs

Productive

Relation

ZMod

Aut

Basic

Coprime

Defs

Factorial

IntUnitsPower

QuotientGroup

QuotientRing

Units

ValMinAbs

BitVec

Bracket

Bundle

Char

Erased

Finmap

Holor

Ineq

Opposite

PEquiv

PFun

Part

Quot

Rel

SProd

Semiquot

Sign

Subtype

TwoPointing

TypeVec

UInt

ULift

Vector3

Deprecated

Aliases

AnalyticManifold

Order

RingHom

Dynamics

BirkhoffSum

Average

Basic

NormedSpace

Circle

RotationNumber

TranslationNumber

Ergodic

Action

Basic

OfMinimal

Regular

AddCircle

AddCircleAdd

Conservative

Ergodic

Extreme

Function

MeasurePreserving

RadonNikodym

FixedPoints

Basic

Prufer

Topology

PeriodicPts

Defs

Lemmas

TopologicalEntropy

CoverEntropy

DynamicalEntourage

NetEntropy

Semiconj

Subset

Flow

Minimal

Newton

OmegaLimit

FieldTheory

Differential

Basic

Liouville

Finite

Basic

GaloisField

Polynomial

Trace

Galois

Basic

GaloisClosure

Infinite

IsGaloisGroup

Profinite

IntermediateField

Adjoin

Algebra

Basic

Defs

Algebraic

Basic

IsAlgClosed

AlgebraicClosure

Basic

Classification

Spectrum

Minpoly

Basic

Field

IsConjRoot

IsIntegrallyClosed

MinpolyDiv

MvRatFunc

Rank

Normal

Basic

Closure

Defs

PurelyInseparable

Basic

Exponent

PerfectClosure

Tower

RatFunc

AsPolynomial

Basic

Defs

Degree

SplittingField

Construction

IsSplittingField

AbelRuffini

AbsoluteGaloisGroup

AlgebraicClosure

AxGrothendieck

CardinalEmb

Cardinality

ChevalleyWarning

Extension

Finiteness

Fixed

IsPerfectClosure

IsSepClosed

Isaacs

JacobsonNoether

KrullTopology

KummerExtension

KummerPolynomial

Laurent

LinearDisjoint

NormalizedTrace

Perfect

PerfectClosure

PolynomialGaloisGroup

PrimitiveElement

Relrank

Separable

SeparableClosure

SeparableDegree

Tower

Geometry

Convex

Cone

Basic

Dual

Pointed

Euclidean

Angle

Oriented

Affine

Basic

RightAngle

Rotation

Unoriented

Affine

Basic

Conformal

CrossProduct

RightAngle

Sphere

Inversion

Basic

Calculus

ImageHyperplane

Sphere

Basic

Power

Ptolemy

SecondInter

Tangent

Altitude

Basic

Circumcenter

Congruence

Incenter

MongePoint

PerpBisector

Projection

SignedDist

Simplex

Triangle

Group

Growth

LinearLowerBound

QuotientInter

Manifold

Algebra

LeftInvariantDerivation

LieGroup

Monoid

SmoothFunctions

Structures

ContMDiff

Atlas

Basic

Constructions

Defs

NormedSpace

Instances

Icc

Real

Sphere

UnitsOfNormedAlgebra

IntegralCurve

Basic

ExistUnique

Transform

UniformTime

IsManifold

Basic

ExtChartAt

InteriorBoundary

MFDeriv

Atlas

Basic

Defs

FDeriv

NormedSpace

SpecificFunctions

Tangent

UniqueDifferential

Riemannian

Basic

PathELength

Sheaf

Basic

LocallyRingedSpace

Smooth

VectorBundle

Basic

FiberwiseLinear

Hom

MDifferentiable

Pullback

Riemannian

SmoothSection

Tangent

VectorField

LieBracket

Pullback

AnalyticManifold

Bordism

BumpFunction

ChartedSpace

Complex

ConformalGroupoid

ContMDiffMFDeriv

ContMDiffMap

DerivationBundle

Diffeomorph

GroupLieAlgebra

LocalDiffeomorph

LocalInvariantProperties

Metrizable

PartitionOfUnity

PoincareConjecture

WhitneyEmbedding

RingedSpace

LocallyRingedSpace (file)

HasColimits

ResidueField

PresheafedSpace (file)

Gluing

HasColimits

Basic

OpenImmersion

SheafedSpace

Stalks

GroupTheory

Commutator

Basic

Finite

Congruence

Basic

BigOperators

Defs

Hom

Opposite

Coprod

Basic

Coset

Basic

Card

Defs

Coxeter

Basic

Inversion

Length

Matrix

FiniteAbelian

Basic

Duality

FreeGroup

Basic

GeneratorEquiv

IsFreeGroup

NielsenSchreier

Reduce

GroupAction

DomAct

ActionHom

Basic

SubMulAction (file)

OfFixingSubgroup

OfStabilizer

Pointwise

Basic

Blocks

CardCommute

ConjAct

Defs

Embedding

FixedPoints

FixingSubgroup

Hom

IterateAct

Iwasawa

MultiplePrimitivity

MultipleTransitivity

Period

Pointwise

Primitive

Quotient

Ring

Support

Transitive

GroupExtension

Basic

Defs

MonoidLocalization

Away

Basic

Cardinality

DivPairs

Finite

GrothendieckGroup

MonoidWithZero

Order

Order

Min

OreLocalization

Basic

Cardinality

OreSet

Perm

Cycle

Basic

Concrete

Factors

PossibleTypes

Type

Basic

Centralizer

Closure

ClosureSwap

ConjAct

DomMulAct

Fin

Finite

List

Option

Sign

Subgroup

Support

ViaEmbedding

QuotientGroup

Basic

Defs

Finite

SpecificGroups

Alternating (file)

Centralizer

Cyclic

Dihedral

KleinFour

Quaternion

ZGroup

Subgroup

Center

Centralizer

Saturated

Simple

Submonoid

Center

Centralizer

Inverses

Subsemigroup

Center

Centralizer

Abelianization

Archimedean

ArchimedeanDensely

ClassEquation

Commensurable

CommutingProbability

Complement

CoprodI

CosetCover

Divisible

DoubleCoset

EckmannHilton

Exponent

Finiteness

FixedPointFree

Frattini

FreeAbelianGroup

Goursat

HNNExtension

Index

IndexNormal

Nilpotent

NoncommCoprod

NoncommPiCoprod

OrderOfElement

PGroup

PresentedGroup

PushoutI

Rank

RegularWreathProduct

Schreier

SchurZassenhaus

SemidirectProduct

Solvable

Sylow

Torsion

Transfer

InformationTheory

KullbackLeibler

Basic

KLFun

Hamming

Lean

Elab

Tactic

Basic

Term

Expr (file)

Basic

ExtraRecognizers

Rat

ReplaceRec

Meta (file)

RefinedDiscrTree (file)

Basic

Encode

Initialize

Lookup

Basic

CongrTheorems

DiscrTree

KAbstractPositions

Simp

PrettyPrinter

Delaborator

CoreM

EnvExtension

Exception

GoalsLocation

Json

LocalContext

Message

Name

Thunk

LinearAlgebra

AffineSpace

AffineSubspace

Basic

Defs

AffineEquiv

AffineMap

Basis

Combination

ContinuousAffineEquiv

Defs

FiniteDimensional

Independent

Matrix

Midpoint

MidpointZero

Ordered

Pointwise

Restrict

Slope

Alternating

Uncurry

Fin

Basic

Curry

DomCoprod

Basis

Basic

Bilinear

Cardinality

Defs

Exact

Fin

Flag

Prod

SMul

Submodule

VectorSpace

BilinearForm

Basic

DualLattice

Hom

Orthogonal

Properties

TensorProduct

Charpoly

BaseChange

Basic

ToMatrix

CliffordAlgebra

BaseChange

Basic

CategoryTheory

Conjugation

Contraction

Equivs

Even

EvenEquiv

Fold

Grading

Inversion

Prod

SpinGroup

Star

Dimension

Torsion

Basic

Finite

Basic

Constructions

DivisionRing

ErdosKaplansky

Finite

Finrank

Free

FreeAndStrongRankCondition

LinearMap

Localization

RankNullity

StrongRankCondition

Subsingleton

DirectSum

Basis

Finsupp

TensorProduct

Dual

Basis

Defs

Lemmas

Eigenspace

Basic

Matrix

Minpoly

Pi

Semisimple

Triangularizable

Zero

ExteriorAlgebra

Basic

Grading

OfAlternating

ExteriorPower

Basic

Pairing

FiniteDimensional

Basic

Defs

Lemmas

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

CardQuotient

Matrix

Quotient

Basic

Determinant

IdealQuotient

Int

ModN

Norm

PID

StrongRankCondition

FreeProduct

Basic

LinearIndependent

Basic

Defs

Lemmas

Matrix

Charpoly

Basic

Coeff

Eigs

FiniteField

LinearMap

Minpoly

Univ

Determinant

Basic

Misc

TotallyUnimodular

GeneralLinearGroup

Basic

Card

Defs

AbsoluteValue

Adjugate

BaseChange

Basis

BilinearForm

Block

Circulant

Diagonal

DotProduct

Dual

FiniteDimensional

FixedDetMatrices

Gershgorin

Hermitian

HermitianFunctionalCalculus

Ideal

Integer

InvariantBasisNumber

IsDiag

LDL

MvPolynomial

Nondegenerate

NonsingularInverse

Orthogonal

Permanent

Permutation

Polynomial

PosDef

ProjectiveSpecialLinearGroup

Reindex

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

Spectrum

StdBasis

Swap

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

Unique

ZPow

Multilinear

Basic

Basis

Curry

DFinsupp

FiniteDimensional

Pi

TensorProduct

PerfectPairing

Basic

Matrix

Restrict

Projectivization

Basic

Cardinality

Constructions

Independence

Subspace

QuadraticForm

QuadraticModuleCat (file)

Monoidal

Symmetric

TensorProduct (file)

Isometries

Basic

Basis

Complex

Dual

Isometry

IsometryEquiv

Prod

Real

Quotient

Basic

Defs

Pi

RootSystem

Finite

CanonicalBilinear

G2

Lemmas

Nondegenerate

GeckConstruction

Basic

Lemmas

Base

BaseChange

Basic

CartanMatrix

Chain

Defs

Hom

Irreducible

IsValuedIn

OfBilinear

Reduced

RootPairingCat

RootPositive

WeylGroup

Span

Basic

Defs

SymmetricAlgebra

Basic

Basis

TensorAlgebra

Basic

Basis

Grading

ToTensorPower

TensorPower

Basic

Pairing

TensorProduct

Graded

External

Internal

Associator

Basic

Basis

DirectLimit

Finiteness

Matrix

Opposite

Pi

Prod

Quotient

RightExactness

Subalgebra

Submodule

Tower

Vanishing

AnnihilatingPolynomial

BilinearMap

Coevaluation

Contraction

Countable

CrossProduct

DFinsupp

Determinant

FiniteSpan

FreeAlgebra

GeneralLinearGroup

Goursat

InvariantBasisNumber

Isomorphisms

JordanChevalley

Lagrange

LinearDisjoint

LinearPMap

Orientation

PID

Pi

PiTensorProduct

Prod

Projection

Ray

Reflection

SModEq

Semisimple

SesquilinearForm

StdBasis

SymplecticGroup

Trace

UnitaryGroup

Vandermonde

Logic

Embedding

Basic

Set

Encodable

Basic

Lattice

Pi

Equiv

Fin

Basic

Rotate

Array

Basic

Defs

Embedding

Finset

Fintype

Functor

List

Multiset

Nat

Option

Pairwise

PartialEquiv

Prod

Set

Sum

Function

Basic

Coequalizer

CompTypeclasses

Conjugate

Defs

DependsOn

FiberPartition

FromTypes

Iterate

OfArity

ULift

Godel

GodelBetaFunction

Nontrivial

Basic

Defs

Small

Basic

Defs

List

Set

Basic

Denumerable

ExistsUnique

Hydra

IsEmpty

Lemmas

Nonempty

OpClass

Pairwise

Relation

Relator

Unique

UnivLE

MeasureTheory

Category

MeasCat

Constructions

BorelSpace

Basic

Complex

ContinuousLinearMap

Metric

Metrizable

Order

Real

Polish

Basic

EmbeddingReal

StronglyMeasurable

AddChar

ClosedCompactCylinders

Cylinders

HaarToSphere

Pi

Projective

ProjectiveFamilyContent

SubmoduleQuotient

UnitInterval

Covering

Besicovitch

BesicovitchVectorSpace

DensityTheorem

Differentiation

LiminfLimsup

OneDim

Vitali

VitaliFamily

Function

AEEqFun (file)

DomAct

ConditionalExpectation

AEMeasurable

Basic

CondexpL1

CondexpL2

Indicator

Real

Unique

L1Space

AEEqFun

HasFiniteIntegral

Integrable

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

Defs

Prod

TriangleInequality

Trim

LpSpace

DomAct

Basic

Continuous

Basic

Complete

ContinuousCompMeasurePreserving

ContinuousFunctions

Indicator

SpecialFunctions

Arctan

Basic

Inner

RCLike

Sinc

StronglyMeasurable

AEStronglyMeasurable

Basic

ENNReal

Inner

Lemmas

Lp

AEEqOfIntegral

AEEqOfLIntegral

AEMeasurableOrder

AEMeasurableSequence

ContinuousMapDense

ConvergenceInMeasure

Egorov

EssSup

FactorsThrough

Floor

Holder

Intersectivity

Jacobian

JacobianOneDim

L2Space

LocallyIntegrable

LpOrder

SimpleFunc

SimpleFuncDense

SimpleFuncDenseLp

UnifTight

UniformIntegrable

Group

AEStabilizer

Action

AddCircle

Arithmetic

Convolution

Defs

FundamentalDomain

GeometryOfNumbers

Integral

IntegralConvolution

LIntegral

MeasurableEquiv

Measure

ModularCharacter

Pointwise

Prod

Integral

Bochner (file)

Basic

ContinuousLinearMap

FundThmCalculus

L1

Set

VitaliCaratheodory

IntervalIntegral (file)

Basic

ContDiff

FundThmCalculus

IntegrationByParts

Periodic

Lebesgue (file)

Add

Basic

Countable

DominatedConvergence

Map

Markov

MeasurePreserving

Norm

Sub

RieszMarkovKakutani

Basic

NNReal

Real

Asymptotics

Average

BochnerL1

BoundedContinuousFunction

CircleAverage

CircleIntegral

CircleTransform

DivergenceTheorem

DominatedConvergence

ExpDecay

FinMeasAdditive

FundThmCalculus

Gamma

Indicator

IntegrableOn

IntegralEqImproper

IntegrationByParts

IntervalAverage

Layercake

LebesgueNormedSpace

Marginal

MeanInequalities

PeakFunction

Periodic

Pi

Prod

SetIntegral

SetToL1

TorusIntegral

VitaliCaratheodory

MeasurableSpace

Basic

Card

Constructions

CountablyGenerated

Defs

Embedding

EventuallyMeasurable

Instances

Invariants

MeasurablyGenerated

NCard

Pi

PreorderRestrict

Prod

Measure

Decomposition

Exhaustion

Hahn

IntegralRNDeriv

Lebesgue

RadonNikodym

Haar

Basic

Disintegration

DistribChar

InnerProductSpace

NormedSpace

OfBasis

Quotient

Unique

Lebesgue

Basic

Complex

EqHaar

Integral

VolumeOfBalls

Typeclasses (file)

Finite

NoAtoms

Probability

SFinite

AEDisjoint

AEMeasurable

AbsolutelyContinuous

AddContent

CharacteristicFunction

Comap

Complex

Content

ContinuousPreimage

Count

Dirac

DiracProba

Doubling

EverywherePos

FiniteMeasure

FiniteMeasureExt

FiniteMeasureProd

GiryMonad

HasOuterApproxClosed

Hausdorff

IntegralCharFun

LevyProkhorovMetric

LogLikelihoodRatio

Map

MeasureSpace

MeasureSpaceDef

MutuallySingular

NullMeasurable

OpenPos

Portmanteau

ProbabilityMeasure

Prod

QuasiMeasurePreserving

Real

Regular

RegularityCompacts

Restrict

SeparableMeasure

Stieltjes

Sub

Tight

TightNormed

Tilted

Trim

WithDensity

WithDensityFinite

Order

Group

Lattice

Lattice

UpperLower

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfAddContent

OfFunction

Operations

SpecificCodomains

ContinuousMap

ContinuousMapZero

VectorMeasure

Decomposition

Hahn

Jordan

JordanSub

Lebesgue

RadonNikodym

Basic

WithDensity

PiSystem

SetAlgebra

SetSemiring

Topology

ModelTheory

Algebra

Field

Basic

CharP

IsAlgClosed

Ring

Basic

Definability

FreeCommRing

Basic

Bundled

Complexity

Definability

DirectLimit

ElementaryMaps

ElementarySubstructures

Encoding

Equivalence

FinitelyGenerated

Fraisse

Graph

LanguageMap

Order

PartialEquiv

Quotients

Satisfiability

Semantics

Skolem

Substructures

Syntax

Types

Ultraproducts

NumberTheory

ClassNumber

AdmissibleAbs

AdmissibleAbsoluteValue

AdmissibleCardPowDegree

Finite

FunctionField

Cyclotomic

Basic

CyclotomicCharacter

Discriminant

Embeddings

Gal

PID

PrimitiveRoots

Rat

Three

DiophantineApproximation

Basic

ContinuedFractions

DirichletCharacter

Basic

Bounds

GaussSum

Orthogonality

EulerProduct

Basic

DirichletLSeries

ExpLog

FLT

Basic

Four

MasonStothers

Polynomial

Three

Harmonic

Bounds

Defs

EulerMascheroni

GammaDeriv

Int

ZetaAsymp

JacobiSum

Basic

LSeries

AbstractFuncEq

Basic

Convergence

Convolution

Deriv

Dirichlet

DirichletContinuation

HurwitzZeta

HurwitzZetaEven

HurwitzZetaOdd

HurwitzZetaValues

Injectivity

Linearity

MellinEqDirichlet

Nonvanishing

Positivity

PrimesInAP

RiemannZeta

SumCoeff

ZMod

LegendreSymbol

QuadraticChar

Basic

GaussSum

AddCharacter

Basic

GaussEisensteinLemmas

JacobiSymbol

QuadraticReciprocity

ZModChar

ModularForms

EisensteinSeries

Basic

Defs

IsBoundedAtImInfty

MDifferentiable

Summable

UniformConvergence

JacobiTheta

Bounds

Manifold

OneVariable

TwoVariable

Basic

CongruenceSubgroups

Identities

LevelOne

QExpansion

SlashActions

SlashInvariantForms

MulChar

Basic

Duality

Lemmas

NumberField

CanonicalEmbedding

Basic

ConvexBody

FundamentalCone

NormLeOne

PolarCoord

Discriminant

Basic

Defs

Different

Ideal (file)

Asymptotics

Basic

KummerDedekind

InfinitePlace

Basic

Embeddings

Ramification

TotallyRealComplex

Units

Basic

DirichletTheorem

Regulator

AdeleRing

Basic

CMField

ClassNumber

Completion

DedekindZeta

Embeddings

EquivReindex

FinitePlaces

FractionalIdeal

House

Norm

ProductFormula

Padics

PadicVal

Basic

Defs

AddChar

Complex

Hensel

MahlerBasis

PadicIntegers

PadicNorm

PadicNumbers

ProperSpace

RingHoms

ValuativeRel

RamificationInertia

Basic

Galois

Unramified

Transcendental

Lindemann

AnalyticalPart

Liouville

Basic

LiouvilleNumber

LiouvilleWith

Measure

Residual

Zsqrtd

Basic

GaussianInt

QuadraticReciprocity

ToReal

ADEInequality

AbelSummation

ArithmeticFunction

Basic

Bernoulli

BernoulliPolynomials

Bertrand

Dioph

Divisors

EllipticDivisibilitySequence

FactorisationProperties

Fermat

FermatPsp

FrobeniusNumber

FunctionField

GaussSum

KummerDedekind

LucasLehmer

LucasPrimality

MaricaSchoenheim

Modular

Multiplicity

Ostrowski

Pell

PellMatiyasevic

PrimeCounting

PrimesCongruentOne

Primorial

PythagoreanTriples

Rayleigh

SelbergSieve

SiegelsLemma

SmoothNumbers

SumFourSquares

SumPrimeReciprocals

SumTwoSquares

VonMangoldt

WellApproximable

Wilson

ZetaValues

Order

Atoms (file)

Finite

BooleanAlgebra (file)

Basic

Defs

Set

BoundedOrder

Basic

Lattice

Monotone

Bounds

Basic

Defs

Image

Lattice

OrderIso

Category

BddDistLat

BddLat

BddOrd

BoolAlg

CompleteLat

DistLat

FinBddDistLat

FinBoolAlg

FinPartOrd

Frm

HeytAlg

Lat

LinOrd

NonemptyFinLinOrd

OmegaCompletePartialOrder

PartOrd

Preord

Semilat

Circular (file)

ZMod

CompactlyGenerated

Basic

Intervals

CompleteLattice

Basic

Chain

Defs

Finset

Group

Lemmas

SetLike

ConditionallyCompleteLattice

Basic

Defs

Finset

Group

Indexed

Defs

LinearOrder

PartialOrder

Unbundled

Extension

Linear

Well

Filter

AtTopBot

Archimedean

Basic

BigOperators

CompleteLattice

CountablyGenerated

Defs

Disjoint

Field

Finite

Finset

Floor

Group

Map

ModEq

Monoid

Prod

Ring

Tendsto

Bases

Basic

Finite

Germ

Basic

OrderedMonoid

Ultrafilter

Basic

Defs

Basic

CardinalInter

Cocardinal

Cofinite

CountableInter

CountableSeparatingOn

CountablyGenerated

Curry

Defs

ENNReal

EventuallyConst

Extr

FilterProduct

Finite

IndicatorFunction

Interval

IsBounded

Ker

Lift

ListTraverse

Map

NAry

Partial

Pi

Pointwise

Prod

Ring

SmallSets

Subsingleton

Tendsto

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

Fin

Nat

SuccPred

Set

Basic

Defs

Disjoint

Fin

Final

Image

Infinite

InitialSeg

IsoIoo

Limit

LinearOrder

Monotone

OrdConnected

OrdConnectedComponent

OrdConnectedLinear

OrderEmbedding

OrderIso

Pi

ProjIcc

SuccOrder

SuccPred

SurjOn

Union

UnorderedInterval

WithBotTop

Basic

Lex

Multiset

Monotone

Basic

Defs

Extension

Monovary

MonovaryOrder

Odd

Union

Partition

Basic

Equipartition

Finpartition

Preorder

Chain

Finite

Prod

Lex

Hom

Rel

GaloisConnection

RelIso

Basic

Set

SuccPred

Archimedean

Basic

CompleteLinearOrder

InitialSeg

IntervalSucc

Limit

LinearLocallyFinite

Relation

Tree

WithBot

UpperLower

Basic

Closure

CompleteLattice

Fibration

Hom

LocallyFinite

Principal

Prod

Relative

Antichain

Antisymmetrization

Basic

Birkhoff

BooleanGenerators

BooleanSubalgebra

Booleanisation

Bounded

Chain

Closure

Cofinal

Comparable

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

CompletePartialOrder

CompleteSublattice

Concept

Copy

CountableDenseLinearOrder

Cover

Directed

DirectedInverseSystem

Disjoint

Disjointed

Estimator

FixedPoints

GameAdd

Grade

Height

Ideal

InitialSeg

Irreducible

IsNormal

Iterate

JordanHolder

KonigLemma

KrullDimension

Lattice

LatticeIntervals

LiminfLimsup

Max

MinMax

Minimal

ModularLattice

Nat

Notation

Nucleus

OmegaCompletePartialOrder

OrdContinuous

OrderIsoNat

PFilter

Part

PartialSups

PiLex

PrimeIdeal

PrimeSeparator

PropInstances

Radical

RelClasses

RelSeries

Restriction

ScottContinuity

SemiconjSup

Set

SetIsMax

SetNotation

Shrink

Sublattice

SupClosed

SupIndep

SymmDiff

Synonym

TransfiniteIteration

TypeTags

ULift

WellFounded

WellFoundedSet

WellQuasiOrder

WithBot

Zorn

ZornAtoms

Probability

Distributions

Gaussian (file)

Basic

Real

Exponential

Gamma

Geometric

Pareto

Poisson

Uniform

Independence

Basic

Conditional

Integrable

Kernel

ZeroOne

Kernel

Composition

AbsolutelyContinuous

Comp

CompMap

CompNotation

CompProd

IntegralCompProd

Lemmas

MapComap

MeasureComp

MeasureCompProd

ParallelComp

Prod

Disintegration

Basic

CDFToKernel

CondCDF

Density

Integral

MeasurableStieltjes

StandardBorel

Unique

IonescuTulcea

Maps

PartialTraj

Traj

Basic

CompProdEqIff

CondDistrib

Condexp

Defs

Integral

Invariance

MeasurableIntegral

MeasurableLIntegral

Posterior

Proper

RadonNikodym

SetIntegral

WithDensity

Martingale

Basic

BorelCantelli

Centering

Convergence

OptionalSampling

OptionalStopping

Upcrossing

Moments

Basic

ComplexMGF

Covariance

CovarianceBilin

IntegrableExpMul

MGFAnalytic

SubGaussian

Tilted

Variance

ProbabilityMassFunction

Basic

Binomial

Constructions

Integrals

Monad

Process

Adapted

Filtration

HittingTime

Kolmogorov

PartitionFiltration

Stopping

BorelCantelli

CDF

CondVar

ConditionalExpectation

ConditionalProbability

Density

IdentDistrib

Integration

Notation

ProductMeasure

StrongLaw

UniformOn

Variance

RepresentationTheory

GroupCohomology

Basic

Functoriality

Hilbert90

LowDegree

Resolution

Homological

GroupCohomology

Basic

Functoriality

Hilbert90

LongExactSequence

LowDegree

Shapiro

GroupHomology

Basic

Functoriality

LowDegree

Shapiro

Resolution

Basic

Character

Coinduced

Coinvariants

FDRep

FiniteIndex

Induced

Invariants

Maschke

Rep

Submodule

Tannaka

RingTheory

AdicCompletion

Algebra

AsTensorProduct

Basic

Exactness

Functoriality

LocalRing

Noetherian

Adjoin

Basic

Dimension

FG

Field

Polynomial

PowerBasis

Tower

Algebraic

Basic

Cardinality

Defs

Integral

LinearIndependent

MvPolynomial

Pi

AlgebraicIndependent

Adjoin

AlgebraicClosure

Basic

Defs

RankAndCardinality

TranscendenceBasis

Transcendental

Artinian

Algebra

Instances

Module

Ring

Bialgebra

Basic

Equiv

Hom

MonoidAlgebra

TensorProduct

Coalgebra

Basic

Equiv

Hom

MonoidAlgebra

TensorProduct

Congruence

Basic

BigOperators

Defs

Opposite

Coprime

Basic

Ideal

Lemmas

DedekindDomain

AdicValuation

Basic

Different

Dvr

Factorization

FiniteAdeleRing

Ideal

Instances

IntegralClosure

PID

SInteger

SelmerGroup

Derivation

Basic

DifferentialRing

Lie

MapCoeffs

ToSquareZero

DiscreteValuationRing

Basic

TFAE

DividedPowers

Basic

DPMorphism

SubDPIdeal

Etale

Basic

Field

Kaehler

Pi

Extension (file)

Cotangent

Basic

LocalizationAway

Presentation

Basic

Basic

Generators

FilteredAlgebra

Basic

Finiteness

Basic

Bilinear

Cardinality

Defs

Finsupp

Ideal

Lattice

Nakayama

Nilpotent

Prod

Projective

Quotient

Small

Subalgebra

Flat

FaithfullyFlat

Algebra

Basic

Basic

CategoryTheory

Domain

Equalizer

EquationalCriterion

Localization

Stability

FractionalIdeal

Basic

Extended

Norm

Operations

GradedAlgebra

Homogeneous

Ideal

Submodule

Basic

FiniteType

HomogeneousLocalization

Noetherian

Radical

HahnSeries

Addition

Basic

HEval

Lex

Multiplication

PowerSeries

Summable

Valuation

HopfAlgebra

Basic

MonoidAlgebra

TensorProduct

Ideal

AssociatedPrime (file)

Basic

Finiteness

Localization

MinimalPrime

Basic

Localization

Norm

AbsNorm

RelNorm

Quotient

Basic

Defs

Index

Nilpotent

Noetherian

Operations

PowTransition

Basic

Basis

BigOperators

Colon

Cotangent

Defs

GoingDown

GoingUp

Height

IdempotentFG

Int

IsPrimary

IsPrincipal

IsPrincipalPowQuotient

KrullsHeightTheorem

Lattice

Maps

Maximal

NatInt

Nonunits

Operations

Over

Pointwise

Prime

Prod

Span

Int

Basic

IntegralClosure

Algebra

Basic

Defs

IsIntegral

Basic

Defs

IsIntegralClosure

Basic

Defs

IntegralRestrict

IntegrallyClosed

Invariant (file)

Basic

Defs

Profinite

Jacobson

Artinian

Ideal

Polynomial

Radical

Ring

Semiprimary

Kaehler

Basic

CotangentComplex

JacobiZariski

Polynomial

TensorProduct

KrullDimension

Basic

Field

Module

NonZeroDivisors

PID

Polynomial

Zero

LocalProperties

Basic

Exactness

IntegrallyClosed

Projective

Reduced

Submodule

LocalRing

MaximalIdeal

Basic

Defs

ResidueField

Algebraic

Basic

Defs

Fiber

Ideal

Instances

RingHom

Basic

Basic

Defs

LocalSubring

Module

NonLocalRing

Quotient

Subring

Localization

Away

AdjoinRoot

Basic

Lemmas

Algebra

AsSubring

AtPrime

BaseChange

Basic

Cardinality

Defs

Finiteness

FractionRing

Free

Ideal

Integer

Integral

InvSubmonoid

LocalizationLocalization

Module

NormTrace

NumDen

Pi

Submodule

Morita

Basic

MvPolynomial (file)

MonomialOrder (file)

DegLex

Symmetric

Defs

FundamentalTheorem

NewtonIdentities

Basic

EulerIdentity

FreeCommRing

Groebner

Homogeneous

Ideal

Localization

Tower

WeightedHomogeneous

MvPowerSeries

Basic

Evaluation

Inverse

LexOrder

LinearTopology

NoZeroDivisors

Order

PiTopology

Substitution

Trunc

Nilpotent

Basic

Defs

Exp

Lemmas

Noetherian

Basic

Defs

Filter

Nilpotent

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Basic

Defs

Transitivity

OreLocalization

Basic

Cardinality

OreSet

Ring

Perfectoid

Untilt

Polynomial

Cyclotomic

Basic

Eval

Expand

Roots

Eisenstein

Basic

Criterion

Distinguished

Generalized

IsIntegral

Hermite

Basic

Gaussian

Resultant

Basic

Basic

Bernstein

Chebyshev

Content

ContentIdeal

DegreeLT

Dickson

GaussLemma

GaussNorm

HilbertPoly

Ideal

IntegralNormalization

IrreducibleRing

Nilpotent

Opposites

Pochhammer

Quotient

Radical

RationalRoot

ScaleRoots

Selmer

SeparableDegree

ShiftedLegendre

SmallDegreeVieta

Tower

UniqueFactorization

Vieta

Wronskian

PolynomialLaw

Basic

PowerSeries

Basic

Binomial

CoeffMulMem

Derivative

Evaluation

GaussNorm

Inverse

NoZeroDivisors

Order

PiTopology

Substitution

Trunc

WeierstrassPreparation

WellKnown

Regular

Category

Depth

IsSMulRegular

RegularSequence

RingHom

Etale

Finite

FinitePresentation

FiniteType

Flat

Injective

Integral

Locally

Smooth

StandardSmooth

Surjective

Unramified

RootsOfUnity

AlgebraicallyClosed

Basic

Complex

EnoughRootsOfUnity

Lemmas

Minpoly

PrimitiveRoots

SimpleModule

Basic

IsAlgClosed

Isotypic

Rank

WedderburnArtin

SimpleRing

Basic

Congr

Defs

Field

Matrix

Smooth

Basic

Kaehler

Local

Locus

Pi

StandardSmooth

StandardSmoothCotangent

Spectrum

Maximal

Basic

Defs

Localization

Topology

Prime

Basic

Chevalley

ChevalleyComplexity

ConstructibleSet

Defs

FreeLocus

Homeomorph

IsOpenComapC

Jacobson

LTSeries

Module

Noetherian

Polynomial

RingHom

TensorProduct

Topology

TensorProduct

Basic

DirectLimitFG

Finite

Free

IsBaseChangePi

MvPolynomial

Nontrivial

Pi

Quotient

Trace

Basic

Defs

Quotient

TwoSidedIdeal

Basic

BigOperators

Instances

Kernel

Lattice

Operations

UniqueFactorizationDomain

Basic

Defs

FactorSet

Finite

Finsupp

GCDMonoid

Ideal

Multiplicative

Multiplicity

Nat

NormalizedFactors

Unramified

Basic

Field

Finite

LocalRing

Locus

Pi

Valuation

Discrete

Basic

AlgebraInstances

Archimedean

Basic

ExtendToLocalization

Extension

Integers

Integral

IntegrallyClosed

LocalSubring

Minpoly

PrimeMultiplicity

Quotient

RamificationGroup

RankOne

ValExtension

ValuationRing

ValuationSubring

ValuativeRel

WittVector

Basic

Compare

Complete

Defs

DiscreteValuationRing

Domain

Frobenius

FrobeniusFractionField

Identities

InitTail

IsPoly

Isocrystal

MulCoeff

MulP

StructurePolynomial

Teichmuller

Truncated

Verschiebung

WittPolynomial

ZMod (file)

UnitsCyclic

AdjoinRoot

AlgebraTower

Bezout

Binomial

ChainOfDivisors

ClassGroup

Complex

CotangentLocalizationAway

Discriminant

DualNumber

EisensteinCriterion

EssentialFiniteness

EuclideanDomain

Filtration

FiniteLength

FinitePresentation

FiniteStability

FiniteType

Fintype

FreeCommRing

FreeRing

Frobenius

Generators

Grassmannian

Henselian

HopkinsLevitzki

Idempotents

IntegralDomain

IsAdjoinRoot

IsPrimary

IsTensorProduct

Lasker

LaurentSeries

Length

LinearDisjoint

LittleWedderburn

MatrixAlgebra

MatrixPolynomialAlgebra

Multiplicity

Nakayama

NoetherNormalization

NormTrace

Nullstellensatz

OrderOfVanishing

OrzechProperty

Perfection

PiTensorProduct

PolynomialAlgebra

PowerBasis

Presentation

Prime

PrincipalIdealDomain

PrincipalIdealDomainOfPrime

QuotSMulTop

Radical

ReesAlgebra

RingHomProperties

RingInvo

Support

SurjectiveOnStalks

SetTheory

Cardinal

Aleph

Arithmetic

Basic

Cofinality

Continuum

CountableCover

Defs

Divisibility

ENat

Embedding

Finite

Finsupp

Free

HasCardinalLT

NatCount

Order

Ordinal

Pigeonhole

Regular

SchroederBernstein

Subfield

ToNat

UnivLE

Descriptive

Tree

Game

Basic

Birthday

Domineering

Impartial

Nim

Ordinal

Short

State

Nimber

Basic

Field

Ordinal

Arithmetic

Basic

CantorNormalForm

Enum

Exponential

Family

FixedPoint

FixedPointApproximants

NaturalOps

Notation

Principal

Rank

Topology

Veblen

PGame

Algebra

Basic

Order

Surreal

Basic

Dyadic

Multiplication

ZFC

Basic

Class

Ordinal

PSet

Rank

Lists

Std

Data

HashMap

Tactic (file)

ArithMult (file)

Init

Attr

Core

Register

Bound (file)

Attribute

Init

CC (file)

Addition

Datatypes

Lemmas

MkProof

CancelDenoms (file)

Core

CategoryTheory

Bicategory

Basic

Datatypes

Normalize

PureCoherence

Coherence (file)

Basic

Datatypes

Normalize

PureCoherence

Monoidal

Basic

Datatypes

Normalize

PureCoherence

BicategoricalComp

BicategoryCoherence

CheckCompositions

Elementwise

IsoReassoc

MonoidalComp

Reassoc

Slice

ToApp

Continuity (file)

Init

Explode (file)

Datatypes

Pretty

Finiteness (file)

Attr

FunProp (file)

Attr

ContDiff

Core

Decl

Differentiable

Elab

FunctionData

Mor

Theorems

ToBatteries

Types

GCongr (file)

Core

CoreAttrs

ForwardAttr

GRewrite (file)

Core

Elab

Linarith (file)

Oracle

SimplexAlgorithm (file)

Datatypes

Gauss

PositiveVector

SimplexAlgorithm

FourierMotzkin

Datatypes

Frontend

Lemmas

Parsing

Preprocessing

Verification

LinearCombination (file)

Lemmas

Linter (file)

CommandStart

DeprecatedModule

DeprecatedSyntaxLinter

DirectoryDependency

DocPrime

DocString

FlexibleLinter

GlobalAttributeIn

HashCommandLinter

HaveLetLinter

Header

Lint

MinImports

Multigoal

OldObtain

PPRoundtrip

Style

TextBased

UnusedTactic

UnusedTacticExtension

UpstreamableDecl

Measurability (file)

Init

Monotonicity (file)

Attr

Basic

Lemmas

Nontriviality (file)

Core

NormNum (file)

Basic

BigOperators

Core

DivMod

Eq

GCD

Ineq

Inv

Irrational

IsCoprime

LegendreSymbol

NatFactorial

NatFib

NatLog

NatSqrt

OfScientific

Pow

PowMod

Prime

RealSqrt

Result

Order (file)

Graph

Basic

Tarjan

CollectFacts

Preprocessing

Positivity (file)

Basic

Core

Finset

ReduceModChar (file)

Ext

Relation

Rfl

Symm

Ring (file)

Basic

Compare

NamePolyVars

PNat

RingNF

Sat

FromLRAT

Simproc

Divisors

ExistsAndEq

Factors

Simps

Basic

NotationClass

ToAdditive (file)

Frontend

Widget

Calc

CommDiag

CongrM

Conv

GCongr

InteractiveUnfold

LibraryRewrite

SelectInsertParamsClass

SelectPanelUtils

StringDiagram

Abel

AdaptationNote

Algebraize

ApplyAt

ApplyCongr

ApplyFun

ApplyWith

Basic

ByContra

Cases

CasesM

Change

Check

Choose

Clean

ClearExcept

ClearExclamation

Clear_

Coe

Common

ComputeDegree

CongrExclamation

CongrM

Constructor

ContinuousFunctionalCalculus

Contrapose

Conv

Convert

Core

DeclarationNames

DefEqTransformations

DeprecateTo

DeriveCountable

DeriveEncodable

DeriveFintype

DeriveTraversable

ENatToNat

Eqns

ErwQuestion

Eval

ExistsI

ExtendDoc

ExtractGoal

ExtractLets

FBinop

FailIfNoProgress

FastInstance

FieldSimp

FinCases

Find

FindSyntax

Generalize

GeneralizeProofs

Group

GuardGoalNums

GuardHypNums

Have

HaveI

HigherOrder

Hint

ITauto

InferParam

Inhabit

IntervalCases

IrreducibleDef

Lemma

Lift

LiftLets

LinearCombination'

MinImports

MkIffOfInductiveProp

ModCases

Module

MoveAdd

NoncommRing

NthRewrite

Observe

OfNat

PNatToNat

PPWithUniv

Peel

Polyrith

ProdAssoc

Propose

ProxyType

Push

Qify

RSuffices

Recall

Recover

Rename

RenameBVar

Replace

RewriteSearch

Rify

Says

ScopedNS

Set

SetLike

SimpIntro

SimpRw

SplitIfs

Spread

StacksAttribute

Subsingleton

Substs

SuccessIfFailWithMsg

SudoSetOption

SuppressCompilation

SwapVar

TFAE

Tauto

TautoSet

TermCongr

ToExpr

ToLevel

Trace

TryThis

TypeCheck

TypeStar

UnsetOption

Use

Variable

WLOG

WithoutCDot

Zify

Testing

Plausible

Functions

Sampleable

Testable

Topology

Algebra

Algebra (file)

Equiv

Rat

Category

ProfiniteGrp

Basic

Limits

Constructions (file)

DomMulAct

Group

Basic

ClosedSubgroup

Compact

CompactOpen

Defs

GroupTopology

OpenMapping

Pointwise

Quotient

SubmonoidClosure

TopologicalAbelianization

InfiniteSum

Basic

Constructions

Defs

ENNReal

Field

Group

GroupCompletion

Module

NatInt

Nonarchimedean

Order

Real

Ring

UniformOn

IsUniformGroup

Basic

Defs

Order

MetricSpace

Lipschitz

Module

Alternating

Basic

Topology

Multilinear

Basic

Bounded

Topology

Basic

Cardinality

CharacterSpace

ClosedSubmodule

Compact

Determinant

Equiv

FiniteDimension

LinearMap

LinearMapPiProd

LinearPMap

LocallyConvex

ModuleTopology

PerfectPairing

PerfectSpace

Simple

Star

StrongTopology

UniformConvergence

WeakBilin

WeakDual

Monoid (file)

AddChar

Defs

Nonarchimedean

AdicTopology

Bases

Basic

Completion

TotallyDisconnected

Order

Archimedean

Field

Floor

Group

LiminfLimsup

Module

Support

UpperLower

ProperAction

Basic

ProperlyDiscontinuous

RestrictedProduct (file)

Basic

TopologicalSpace

Ring

Basic

Compact

Ideal

Real

SeparationQuotient

Basic

FiniteDimensional

Hom

Section

Star (file)

Real

Unitary

Valued

LocallyCompact

NormedValued

ValuationTopology

ValuativeRel

ValuedField

WithVal

WithZeroMulInt

Affine

AffineSubspace

ClopenNhdofOne

ClosedSubgroup

ConstMulAction

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

IntermediateField

IsOpenUnits

LinearTopology

Localization

MulAction

MvPolynomial

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

PontryaginDual

ProperConstSMul

Semigroup

StarSubalgebra

Support

TopologicallyNilpotent

UniformConvergence

UniformField

UniformFilterBasis

UniformMulAction

UniformRing

WithZeroTopology

Baire

BaireMeasurable

CompleteMetrizable

Lemmas

LocallyCompactRegular

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Real

CWComplex

Abstract

Basic

Classical

Basic

Finite

Category

CompHaus

Basic

EffectiveEpi

Frm

Limits

Projective

CompHausLike

Basic

EffectiveEpi

Limits

SigmaComparison

LightProfinite

AsLimit

Basic

EffectiveEpi

Extend

Limits

Sequence

Profinite

Nobeling (file)

Basic

Induction

Span

Successor

ZeroLimit

AsLimit

Basic

CofilteredLimit

EffectiveEpi

Extend

Limits

Product

Projective

Stonean

Adjunctions

Basic

EffectiveEpi

Limits

TopCat

Limits

Basic

Cofiltered

Konig

Products

Pullbacks

Adjunctions

Basic

EffectiveEpi

EpiMono

OpenNhds

Opens

Sphere

ULift

Yoneda

Born

CompactlyGenerated

Compactum

DeltaGenerated

FinTopCat

Locale

Sequential

TopCommRingCat

UniformSpace

Compactification

OnePoint (file)

Basic

ProjectiveLine

Sphere

OnePointEquiv

StoneCech

Compactness

Bases

Compact

CompactlyCoherentSpace

CompactlyGeneratedSpace

DeltaGeneratedSpace

Exterior

HilbertCubeEmbedding

Lindelof

LocallyCompact

LocallyFinite

NhdsKer

Paracompact

PseudometrizableLindelof

SigmaCompact

Connected

Basic

Clopen

LocPathConnected

LocallyConnected

PathComponentOne

PathConnected

Separation

TotallyDisconnected

Constructions (file)

SumProd

ContinuousMap

Bounded

ArzelaAscoli

Basic

Normed

Star

Algebra

Basic

BoundedCompactlySupported

CocompactMap

Compact

CompactlySupported

ContinuousMapZero

ContinuousSqrt

Defs

Ideals

Interval

Lattice

LocallyConstant

LocallyConvex

Ordered

Periodic

Polynomial

SecondCountableSpace

Sigma

Star

StarOrdered

StoneWeierstrass

T0Sierpinski

Units

Weierstrass

ZeroAtInfty

Defs

Basic

Filter

Induced

Sequences

Ultrafilter

EMetricSpace

Basic

BoundedVariation

Defs

Diam

Lipschitz

Paracompact

Pi

FiberBundle

Basic

Constructions

IsHomeomorphicTrivialBundle

Trivialization

GDelta

Basic

MetrizableSpace

UniformSpace

Hom

ContinuousEval

ContinuousEvalConst

Open

Homeomorph

Defs

Lemmas

Homotopy

Basic

Contractible

Equiv

HSpaces

HomotopyGroup

Lifting

Path

Product

Instances

AddCircle

Defs

DenseSubgroup

Real

ENNReal

Lemmas

EReal

Lemmas

NNReal

Lemmas

Real

Lemmas

CantorSet

Complex

Discrete

ENat

Int

Irrational

Matrix

Nat

PNat

Rat

RatLemmas

RealVectorSpace

Shrink

Sign

TrivSqZeroExt

ZMod

ZMultiples

LocallyConstant

Algebra

Basic

Maps

Proper

Basic

CompactlyGenerated

UniversallyClosed

Basic

OpenQuotient

MetricSpace

ProperSpace (file)

Lemmas

Real

Pseudo

Basic

Constructions

Defs

Lemmas

Pi

Real

Ultra

Basic

ContinuousMaps

Pi

TotallySeparated

Algebra

Antilipschitz

Basic

Bilipschitz

Bounded

BundledFun

CantorScheme

CauSeqFilter

Cauchy

Closeds

Completion

Congruence

Contracting

Defs

Dilation

DilationEquiv

Equicontinuity

Gluing

GromovHausdorff

GromovHausdorffRealized

HausdorffDimension

HausdorffDistance

Holder

HolderNorm

Infsep

IsometricSMul

Isometry

Kuratowski

Lipschitz

MetricSeparated

PartitionOfUnity

Perfect

PiNat

Polish

Sequences

ShrinkingLemma

Similarity

ThickenedIndicator

Thickening

UniformConvergence

Metrizable

Basic

CompletelyMetrizable

ContinuousMap

Real

Uniformity

Urysohn

Order (file)

Category

AlexDisc

FrameAdjunction

Hom

Basic

Esakia

Basic

Bornology

Compact

CountableSeparating

DenselyOrdered

ExtendFrom

ExtrClosure

Filter

HullKernel

IntermediateValue

IsLUB

IsLocallyClosed

Lattice

LawsonTopology

LeftRight

LeftRightLim

LeftRightNhds

LiminfLimsup

LocalExtr

LowerUpperTopology

Monotone

MonotoneContinuity

MonotoneConvergence

NhdsSet

OrderClosed

OrderClosedExtr

PartialSups

Priestley

ProjIcc

Real

Rolle

ScottTopology

T5

UpperLowerSetTopology

Separation

Basic

CompletelyRegular

Connected

CountableSeparatingOn

DisjointCover

GDelta

Hausdorff

NotNormal

Profinite

Regular

SeparatedNhds

Sets

Closeds

CompactOpenCovered

Compacts

OpenCover

Opens

Order

Sheaves

SheafCondition

EqualizerProducts

OpensLeCover

PairwiseIntersections

Sites

UniqueGluing

Alexandrov

CommRingCat

Forget

Functors

Init

Limits

LocalPredicate

LocallySurjective

MayerVietoris

PUnit

Presheaf

PresheafOfFunctions

Sheaf

SheafOfFunctions

Sheafify

Skyscraper

Stalks

Spectral

Basic

Hom

Prespectral

UniformSpace

Ultra

Basic

Constructions

AbsoluteValue

AbstractCompletion

Ascoli

Basic

Cauchy

Compact

CompactConvergence

CompareReals

CompleteSeparated

Completion

Defs

Dini

DiscreteUniformity

Equicontinuity

Equiv

HeineCantor

LocallyUniformConvergence

Matrix

OfCompactT2

OfFun

Pi

ProdApproximation

Real

Separation

UniformApproximation

UniformConvergence

UniformConvergenceTopology

UniformEmbedding

VectorBundle

Basic

Constructions

Hom

Riemannian

AlexandrovDiscrete

ApproximateUnit

Bases

Basic

Clopen

ClopenBox

Closure

ClusterPt

Coherent

CompactOpen

Constructible

Continuous

ContinuousOn

Covering

DenseEmbedding

DerivedSet

DiscreteQuotient

DiscreteSubset

ExtendFrom

Exterior

ExtremallyDisconnected

FiberPartition

Filter

Germ

Gluing

IndicatorConstPointwise

Inseparable

Irreducible

IsClosedRestrict

IsLocalHomeomorph

JacobsonSpace

KrullDimension

List

LocalAtTarget

LocallyClosed

LocallyFinite

LocallyFinsupp

Neighborhoods

NhdsKer

NhdsSet

NoetherianSpace

OmegaCompletePartialOrder

Partial

PartialHomeomorph

PartitionOfUnity

Path

Perfect

Piecewise

PreorderRestrict

QuasiSeparated

Semicontinuous

SeparatedMap

Sequences

ShrinkingLemma

Sober

Specialization

StoneCech

TietzeExtension

Ultrafilter

UnitInterval

UrysohnsBounded

UrysohnsLemma

Util

AddRelatedDecl

AssertExists

AssertExistsExt

AssertNoSorry

AtomM

CompileInductive

CountHeartbeats

Delaborators

DischargerAsTactic

Export

FormatTable

GetAllModules

LongNames

MemoFix

Notation3

PPOptions

ParseCommand

Qq

Simp

SleepHeartbeats

Superscript

SynthesizeUsing

Tactic

TermReduce

TransImports

WhatsNew

WithWeakNamespace

Init

Plausible (file)

Attr

Functions

Gen

Random

Sampleable

Tactic

Testable

ProofWidgets (file)

Component

Panel

Basic

GoalTypePanel

SelectionPanel

Basic

FilterDetails

GraphDisplay

HtmlDisplay

InteractiveSvg

MakeEditLink

OfRpcMethod

PenroseDiagram

Recharts

Data

Html

Svg

Presentation

Expr

Cancellable

Compat

Util

Qq (file)

ForLean

Do

ReduceEval

ToExpr

AssertInstancesCommute

Commands

Delab

Macro

Match

MetaM

Simp

SortLocalDecls

Typ

Std (file)

Classes (file)

Ord (file)

Basic

BitVec

SInt

String

UInt

Vector

Data (file)

DHashMap (file)

Internal

AssocList

Basic

Lemmas

Defs

HashesTo

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

Lemmas

Raw

RawDef

RawLemmas

DTreeMap (file)

Internal

WF

Defs

Lemmas

Balanced

Balancing

Cell

Def

Lemmas

Model

Operations

Ordered

Queries

Raw (file)

AdditionalOperations

Basic

Lemmas

WF

AdditionalOperations

Basic

Lemmas

ExtDHashMap (file)

Basic

Lemmas

ExtDTreeMap (file)

Basic

Lemmas

ExtHashMap (file)

Basic

Lemmas

ExtHashSet (file)

Basic

Lemmas

ExtTreeMap (file)

Basic

Lemmas

ExtTreeSet (file)

Basic

Lemmas

HashMap (file)

AdditionalOperations

Basic

Lemmas

Raw

RawLemmas

HashSet (file)

Basic

Lemmas

Raw

RawLemmas

Internal

List

Associative

Defs

Cut

Iterators (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

StepSize

Take

TakeWhile

Zip

Drop

DropWhile

StepSize

Take

TakeWhile

Zip

Lemmas (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

FilterMap

Take

TakeWhile

Zip

Drop

DropWhile

Take

TakeWhile

Zip

Consumers (file)

Monadic (file)

Collect

Loop

Collect

Loop

Equivalence (file)

Basic

HetT

StepCongr

Producers (file)

Monadic (file)

Array

Empty

List

Array

Empty

List

Range

Repeat

Slice

Monadic

Producers (file)

Monadic (file)

Array

Empty

List

Array

Empty

List

Range

Repeat

Slice

TreeMap (file)

Raw (file)

AdditionalOperations

Basic

Lemmas

WF

AdditionalOperations

Basic

Lemmas

TreeSet (file)

Raw (file)

Basic

Lemmas

WF

AdditionalOperations

Basic

Lemmas

Do (file)

SPred (file)

DerivedLaws

Laws

Notation

SPred

SVal

Triple (file)

Basic

SpecLemmas

WP (file)

Basic

IO

Monad

SimpLemmas

PostCond

PredTrans

Internal (file)

Async (file)

Basic

DNS

Process

Select

System

TCP

Timer

UDP

Parsec (file)

Basic

ByteArray

String

UV (file)

DNS

Loop

System

TCP

Timer

UDP

Rat

Net (file)

Addr

Sat (file)

AIG (file)

RefVecOperator (file)

Fold

Map

Zip

Basic

CNF

Cached

CachedGates

CachedGatesLemmas

CachedLemmas

If

LawfulOperator

LawfulVecOperator

Lemmas

RefVec

Relabel

RelabelNat

CNF (file)

Basic

Dimacs

Literal

Relabel

RelabelFin

Sync (file)

Barrier

Basic

Channel

Mutex

RecursiveMutex

SharedMutex

Tactic (file)

BVDecide (file)

Bitblast (file)

BVExpr (file)

Circuit (file)

Impl (file)

Operations

Add

Append

Clz

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

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

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

Format (file)

Basic

Internal (file)

Bounded

UnitVal

Notation (file)

Spec

Time (file)

Unit

Basic

Hour

Millisecond

Minute

Nanosecond

Second

Basic

HourMarker

PlainTime

Zoned (file)

Database (file)

Basic

TZdb

TzIf

Windows

DateTime

Offset

TimeZone

ZoneRules

ZonedDateTime

Duration

docs (file)

Conv

Guide

Introduction

references (file)

Color scheme

darksystemlight