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

Frontend

Extension (file)

Init

Attribute

Basic

Command

RuleExpr

Saturate

Tactic

Index (file)

Basic

DiscrTreeConfig

Options (file)

Internal

Public

Rule (file)

Basic

Name

RuleSet (file)

Filter

Member

Name

RuleTac (file)

Forward (file)

Basic

Apply

Basic

Cases

ElabRuleTerm

FVarIdSubst

GoalDiff

Preprocess

Tactic

Script

Check

CtorNames

GoalWithMVars

Main

OptimizeSyntax

SScript

ScriptM

SpecificTactics

Step

StructureDynamic

StructureStatic

Tactic

TacticState

UScript

UScriptToSScript

Util

Search

Expansion (file)

Basic

Norm

Simp

Queue (file)

Class

ExpandSafePrefix

Main

RuleSelection

SearchM

Stats

Basic

Extension

Report

Tree (file)

AddRapp

Check

Data

ExtractProof

ExtractScript

Free

RunMetaM

State

Tracing

Traversal

TreeM

UnsafeQueue

Util

Tactic (file)

Ext

Unfold

Basic

EqualUpToIds

UnionFind

UnorderedArraySet

Check

Constants

ElabM

Exception

Main

Nanos

Percent

RulePattern

Saturate

Tracing

Archive (file)

Examples

IfNormalization

Result

Statement

WithoutAesop

MersennePrimes

PropEncodable

Imo

Imo1959Q1

Imo1959Q2

Imo1960Q1

Imo1960Q2

Imo1961Q3

Imo1962Q1

Imo1962Q4

Imo1963Q5

Imo1964Q1

Imo1969Q1

Imo1972Q5

Imo1975Q1

Imo1977Q6

Imo1981Q3

Imo1982Q1

Imo1982Q3

Imo1986Q5

Imo1987Q1

Imo1988Q6

Imo1994Q1

Imo1998Q2

Imo2001Q2

Imo2001Q6

Imo2005Q3

Imo2005Q4

Imo2006Q3

Imo2006Q5

Imo2008Q2

Imo2008Q3

Imo2008Q4

Imo2011Q3

Imo2011Q5

Imo2013Q1

Imo2013Q5

Imo2019Q1

Imo2019Q2

Imo2019Q4

Imo2020Q2

Imo2021Q1

Imo2024Q1

Imo2024Q2

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

Lemmas

Data

Array (file)

Init

Lemmas

Basic

Lemmas

Match

Merge

Monadic

OfFn

Pairwise

BinomialHeap (file)

Basic

Lemmas

DList (file)

Basic

Lemmas

Fin (file)

Basic

Fold

Lemmas

HashMap (file)

Basic

Lemmas

WF

List (file)

Init

Lemmas

Basic

Count

EraseIdx

FinRange

Lemmas

Matcher

Monadic

OfFn

Pairwise

Perm

MLList (file)

Basic

Heartbeats

IO

Nat (file)

Basic

Bisect

Gcd

Lemmas

RBMap (file)

Alter

Basic

Depth

Lemmas

WF

Range (file)

Lemmas

Rat (file)

Basic

Float

Lemmas

String (file)

Basic

Lemmas

Matcher

UnionFind (file)

Basic

Lemmas

Vector (file)

Basic

Lemmas

AssocList

BinaryHeap

ByteArray

ByteSubarray

Char

FloatArray

LazyList

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

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

PrintPrefix

SeqFocus

ShowUnused

SqueezeScope

Trans

Unreachable

Where

Util

Cache

ExtendedBinder

LibraryNote

Panic

Pickle

ProofWanted

Logic

WF

Counterexamples (file)

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)

Basic

Instances

Basic

EState

Except

ExceptCps

Id

Option

Reader

State

StateCps

StateRef

Data (file)

Array (file)

Subarray (file)

Split

Attach

Basic

BasicAux

BinSearch

Bootstrap

DecidableEq

FinRange

GetLit

InsertionSort

Lemmas

MapIdx

Mem

Monadic

QSort

Set

TakeDrop

BitVec (file)

Basic

BasicAux

Bitblast

Folds

Lemmas

ByteArray (file)

Basic

Char (file)

Basic

Lemmas

Fin (file)

Basic

Bitwise

Fold

Iterate

Lemmas

Log2

FloatArray (file)

Basic

Format (file)

Basic

Instances

Macro

Syntax

Int (file)

Bitwise (file)

Lemmas

Basic

DivMod

DivModLemmas

Gcd

Lemmas

LemmasAux

Order

Pow

List (file)

Nat (file)

BEq

Basic

Count

Erase

Find

InsertIdx

Modify

Pairwise

Range

Sublist

TakeDrop

Sort (file)

Basic

Impl

Lemmas

Attach

Basic

BasicAux

Control

Count

Erase

FinRange

Find

Impl

Lemmas

MapIdx

MinMax

Monadic

Notation

OfFn

Pairwise

Perm

Range

Sublist

TakeDrop

ToArray

Zip

Nat (file)

Bitwise (file)

Basic

Lemmas

Basic

Compare

Control

Div

Dvd

Fold

Gcd

Lcm

Lemmas

Linear

Log2

MinMax

Mod

Power2

SOM

Simproc

Option (file)

Attach

Basic

BasicAux

Instances

Lemmas

List

SInt (file)

Basic

String (file)

Basic

Extra

Lemmas

Sum (file)

Basic

Lemmas

ToString (file)

Basic

Macro

UInt (file)

Basic

BasicAux

Bitwise

Lemmas

Log2

Vector (file)

Basic

AC

BEq

Basic

Bool

Cast

Channel

Float

Function

Hashable

NeZero

OfScientific

Ord

PLift

Prod

Queue

RArray

Random

Range

Repr

Stream

Subtype

ULift

Zero

Grind (file)

Cases

Lemmas

Norm

Tactics

Omega (file)

Coeffs

Constraint

Int

IntList

LinearCombo

Logic

System (file)

FilePath

IO

IOError

Mutex

Platform

Promise

ST

Uri

BinderPredicates

ByCases

Classical

Coe

Conv

Core

Dynamic

Ext

GetElem

Guard

Hints

MacroTrace

Meta

MetaTypes

Notation

NotationExtra

Prelude

PropLemmas

RCases

ShareCommon

SimpLemmas

Simproc

SizeOf

SizeOfLemmas

Syntax

Tactics

TacticsExtra

Util

WF

WFTactics

While

Lake (file)

Build (file)

Actions

Basic

Common

Data

Executable

Facets

Fetch

Imports

Index

Info

Job

Key

Library

Module

Package

Run

Store

Targets

Topological

Trace

CLI

Actions

Build

Error

Config (file)

Context

Defaults

Dependency

Env

ExternLib

ExternLibConfig

FacetConfig

Glob

InstallPath

LeanConfig

LeanExe

LeanExeConfig

LeanLib

LeanLibConfig

Module

Monad

Opaque

Package

Script

TargetConfig

Workspace

WorkspaceConfig

DSL (file)

Attributes

AttributesCore

Config

DeclUtil

Extensions

Meta

Package

Require

Script

Targets

Load

Config

Toml (file)

Data

DateTime

Dict

Value

Elab (file)

Expression

Value

Grammar

Load

ParserUtil

Util

Binder

Casing

Compare

Cycle

DRBMap

Date

EStateT

EquipT

Error

Exit

Family

FilePath

Git

IO

JsonObject

Lift

List

Lock

Log

Message

Name

NativeLib

Opaque

OrdHashSet

OrderedTagAttribute

Proc

RBArray

Store

StoreInsts

Sugar

Task

Version

Reservoir

Version

Lean (file)

Compiler (file)

IR (file)

Basic

Borrow

Boxing

Checker

CompilerM

CtorLayout

ElimDeadBranches

ElimDeadVars

EmitC

EmitUtil

ExpandResetReuse

Format

FreeVars

LiveVars

NormIds

PushProj

RC

ResetReuse

SimpCase

Sorry

UnboxResult

LCNF (file)

Simp (file)

Basic

Config

ConstantFold

DefaultAlt

DiscrM

FunDeclInfo

InlineCandidate

InlineProj

JpCases

Main

SimpM

SimpValue

Used

AlphaEqv

AuxDeclCache

BaseTypes

Basic

Bind

CSE

Check

Closure

CompatibleTypes

CompilerM

ConfigOptions

DeclHash

DependsOn

ElimDead

ElimDeadBranches

FVarUtil

FixedParams

FloatLetIn

ForEachExpr

InferType

Internalize

JoinPoints

LCtx

LambdaLifting

Level

Main

MonadScope

MonoTypes

OtherDecl

PassManager

Passes

PhaseExt

PrettyPrinter

PullFunDecls

PullLetDecls

ReduceArity

ReduceJpArity

Renaming

ScopeM

SpecInfo

Specialize

Testing

ToDecl

ToExpr

ToLCNF

ToMono

Types

Util

AtMostOnce

BorrowedAnnotation

CSimpAttr

ClosedTermCache

ConstFolding

ExportAttr

ExternAttr

FFI

ImplementedByAttr

InitAttr

InlineAttrs

Main

NameMangling

NeverExtractAttr

NoncomputableAttr

Old

Options

Specialize

Data (file)

Json (file)

Basic

Elab

FromToJson

Parser

Printer

Stream

Lsp (file)

Basic

Capabilities

Client

CodeActions

Communication

Diagnostics

Extra

InitShutdown

Internal

Ipc

LanguageFeatures

TextSync

Utf16

Workspace

Xml (file)

Basic

Parser

Array

AssocList

Format

FuzzyMatching

HashMap

HashSet

JsonRpc

KVMap

LBool

LOption

Name

NameMap

NameTrie

OpenDecl

Options

PersistentArray

PersistentHashMap

PersistentHashSet

Position

PrefixTree

RArray

RBMap

RBTree

SMap

SSet

Trie

DocString (file)

Extension

Elab (file)

Deriving (file)

BEq

Basic

DecEq

FromToJson

Hashable

Inhabited

Nonempty

Ord

Repr

SizeOf

TypeName

Util

InfoTree (file)

Main

Types

PreDefinition (file)

Nonrec

Eqns

Structural (file)

BRecOn

Basic

Eqns

FindRecArg

IndGroupInfo

IndPred

Main

Preprocess

RecArgInfo

SmartUnfolding

WF (file)

Basic

Eqns

Fix

GuessLex

Ite

Main

PackMutual

Preprocess

Rel

Basic

EqUnfold

Eqns

Main

MkInhabitant

TerminationArgument

TerminationHint

Quotation (file)

Precheck

Util

Tactic (file)

BVDecide (file)

Frontend (file)

BVDecide (file)

Reflect

ReifiedBVExpr

ReifiedBVLogical

ReifiedBVPred

ReifiedLemmas

Reify

SatAtBVLogical

Attr

BVCheck

BVTrace

LRAT

Normalize

LRAT (file)

Trim

External

Conv (file)

Basic

Change

Congr

Delta

Pattern

Rewrite

Simp

Unfold

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

Basic

BoolToPropSimps

BuiltinTactic

Cache

Calc

Change

Classical

Config

Congr

Delta

DiscrTreeKey

Doc

ElabTerm

Ext

FalseOrByContra

Generalize

Guard

Induction

Injection

LibrarySearch

Location

Match

Meta

NormCast

RCases

Repeat

Rewrite

Rewrites

Rfl

ShowTerm

Simp

SimpTrace

Simpa

Simproc

SolveByElim

Split

Symm

Unfold

App

Arg

Attributes

AutoBound

AuxDef

BinderPredicates

Binders

BindersUtil

BuiltinCommand

BuiltinEvalCommand

BuiltinNotation

BuiltinTerm

Calc

CheckTactic

Command

ComputedFields

Config

DeclModifiers

DeclNameGen

DeclUtil

Declaration

DeclarationRange

DefView

Do

ElabRules

Eval

Exception

Extra

Frontend

GenInjective

GuardMsgs

Import

Inductive

InheritDoc

LetRec

Level

Macro

MacroArgUtil

MacroRules

Match

MatchAltView

MatchExpr

Mixfix

MutualDef

MutualInductive

Notation

Open

ParseImportsFast

PatternVar

Print

RecAppSyntax

SetOption

StructInst

Structure

Syntax

SyntheticMVars

Term

Time

Util

Language

Lean (file)

Types

Basic

Util

Linter (file)

Basic

Builtin

ConstructorAsVariable

Deprecated

MissingDocs

Omit

UnusedVariables

Util

Meta (file)

ArgsPacker (file)

Basic

Constructions (file)

BRecOn

CasesOn

NoConfusion

RecOn

Match (file)

MatcherApp

Basic

Transform

Basic

CaseArraySizes

CaseValues

Match

MatchEqs

MatchEqsExt

MatchPatternAttr

MatcherInfo

Value

Tactic (file)

AC (file)

Main

Grind (file)

Attr

Cases

Core

Injection

Preprocessor

RevertAll

Types

Util

LinearArith (file)

Nat (file)

Basic

Simp

Solver

Basic

Main

Simp

Solver

Simp (file)

BuiltinSimprocs (file)

Array

BitVec

Char

Core

Fin

Int

List

Nat

String

UInt

Util

Attr

Diagnostics

Main

RegisterCommand

Rewrite

SimpAll

SimpCongrTheorems

SimpTheorems

Simproc

Types

Acyclic

Apply

Assert

Assumption

AuxLemma

Backtrack

Cases

Cleanup

Clear

Congr

Constructor

Contradiction

Delta

ElimInfo

FVarSubst

FunInd

Generalize

IndependentOf

Induction

Injection

Intro

LibrarySearch

NormCast

Refl

Rename

Repeat

Replace

Revert

Rewrite

Rewrites

Rfl

SolveByElim

Split

SplitIf

Subst

Symm

TryThis

Unfold

UnifyEq

Util

ACLt

AbstractMVars

AbstractNestedProofs

AppBuilder

Basic

Canonicalizer

Check

CheckTactic

Closure

Coe

CoeAttr

CollectFVars

CollectMVars

CompletionName

CongrTheorems

CtorRecognizer

DecLevel

Diagnostics

DiscrTree

DiscrTreeTypes

Eqns

Eval

ExprDefEq

ExprLens

ExprTraverse

ForEachExpr

FunInfo

GeneralizeTelescope

GeneralizeVars

GetUnfoldableConst

GlobalInstances

IndPredBelow

Inductive

InferType

Injective

Instances

Iterator

KAbstract

KExprMap

LazyDiscrTree

LevelDefEq

LitValues

MatchUtil

NatInstTesters

Offset

PPGoal

PProdN

RecursorInfo

Reduce

ReduceEval

SizeOf

Structure

SynthInstance

Transform

TransparencyMode

UnificationHint

WHNF

Parser (file)

Tactic (file)

Doc

Attr

Basic

Command

Do

Extension

Extra

Level

Module

StrInterpolation

Syntax

Term

Types

ParserCompiler (file)

Attribute

PrettyPrinter (file)

Delaborator (file)

Attributes

Basic

Builtins

FieldNotation

Options

SubExpr

TopDownAnalyze

Basic

Formatter

Parenthesizer

Server (file)

CodeActions (file)

Attr

Basic

Provider

Completion (file)

CompletionCollectors

CompletionInfoSelection

CompletionItemData

CompletionResolution

CompletionUtils

EligibleHeaderDecls

ImportCompletion

SyntheticCompletion

FileWorker (file)

RequestHandling

SetupFile

Utils

WidgetRequests

Rpc (file)

Basic

Deriving

RequestHandling

AsyncList

FileSource

GoTo

InfoUtils

References

Requests

Snapshots

Utils

Watchdog

Util (file)

CollectAxioms

CollectFVars

CollectLevelMVars

CollectLevelParams

CollectMVars

Diff

FileSetupInfo

FindExpr

FindLevelMVar

FindMVar

FoldConsts

ForEachExpr

ForEachExprWhere

HasConstCache

Heartbeats

InstantiateLevelParams

LakePath

LeanOptions

MonadBacktrack

MonadCache

NumApps

NumObjs

OccursCheck

PPExt

Path

Paths

Profile

Profiler

PtrSet

RecDepth

Recognizers

ReplaceExpr

ReplaceLevel

SCC

SafeExponentiation

SearchPath

ShareCommon

Sorry

TestExtern

Trace

Widget (file)

Basic

Diff

InteractiveCode

InteractiveDiagnostic

InteractiveGoal

TaggedText

Types

UserWidget

AddDecl

Attributes

AuxRecursor

BuiltinDocAttr

Class

CoreM

Declaration

DeclarationRange

Environment

Exception

Expr

HeadIndex

Hygiene

ImportingFlag

InternalExceptionId

KeyedDeclsAttribute

LabelAttribute

Level

LoadDynlib

LocalContext

Log

Message

MetavarContext

Modifiers

MonadEnv

ProjFns

ReducibilityAttrs

Replay

ReservedNameAction

ResolveName

Runtime

ScopedEnvExtension

Structure

SubExpr

Syntax

ToExpr

LeanSearchClient (file)

Basic

LoogleSyntax

Syntax

Mathlib (file)

Algebra

AddConstMap

Basic

Equiv

Algebra

Hom (file)

Rat

Subalgebra

Basic

Directed

IsSimpleOrder

MulOpposite

Operations

Order

Pointwise

Prod

Rank

Tower

Unitization

Basic

Bilinear

Defs

Equiv

Field

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Quasispectrum

Rat

RestrictScalars

Spectrum

Tower

Unitization

ZMod

Associated

Basic

OrderedCommMonoid

BigOperators

Group

Finset

List

Multiset

GroupWithZero

Action

Finset

Ring (file)

List

Multiset

Nat

Associated

Balance

Expect

Fin

Finprod

Finsupp

Intervals

Module

NatAntidiagonal

Option

Pi

RingEquiv

Sym

WithTop

Category

AlgebraCat

Basic

Limits

Monoidal

Symmetric

BialgebraCat

Basic

CoalgebraCat

Basic

ComonEquivalence

Monoidal

FGModuleCat

Basic

Limits

Grp

AB

Abelian

Adjunctions

Basic

Biproducts

Colimits

EnoughInjectives

EpiMono

EquivalenceGroupAddGroup

FilteredColimits

FiniteGrp

ForgetCorepresentable

Images

Injective

Kernels

Limits

Preadditive

Subobject

ZModuleEquivalence

Zero

HopfAlgebraCat

Basic

ModuleCat

Differentials

Basic

Presheaf

Monoidal

Basic

Closed

Symmetric

Presheaf (file)

Abelian

ChangeOfRings

Colimits

EpiMono

Free

Generator

Limits

Monoidal

Pushforward

Sheafification

Sheafify

Sheaf (file)

Abelian

ChangeOfRings

Colimits

Free

Generators

Limits

PushforwardContinuous

Quasicoherent

AB

Abelian

Adjunctions

Algebra

Basic

Biproducts

ChangeOfRings

Colimits

EnoughInjectives

EpiMono

FilteredColimits

Free

Images

Injective

Kernels

Limits

Products

Projective

Pseudofunctor

Simple

Subobject

Tannaka

MonCat

Adjunctions

Basic

Colimits

FilteredColimits

ForgetCorepresentable

Limits

Ring

Under

Basic

Limits

Adjunctions

Basic

Colimits

Constructions

Epi

FilteredColimits

Instances

Limits

LinearAlgebra

Semigrp

Basic

BoolRing

GrpWithZero

Central

Basic

Defs

Matrix

CharP

Algebra

Basic

CharAndCard

Defs

ExpChar

IntermediateField

Invertible

Lemmas

LinearMaps

LocalRing

MixedCharZero

Pi

Quotient

Reduced

Subring

Two

CharZero

Defs

Infinite

Lemmas

Quotient

ContinuedFractions

Computation

ApproximationCorollaries

Approximations

Basic

CorrectnessTerminating

TerminatesIffRat

Translations

Basic

ContinuantsRecurrence

ConvergentsEquiv

Determinant

TerminatedStable

Translations

DirectSum

AddChar

Algebra

Basic

Decomposition

Finsupp

Internal

LinearMap

Module

Ring

Divisibility

Basic

Hom

Prod

Units

Equiv

TransferInstance

EuclideanDomain

Basic

Defs

Field

Int

Field

Subfield

Basic

Defs

Basic

Defs

Equiv

IsField

MinimalAxioms

Opposite

Power

Rat

ULift

FreeAlgebra (file)

Cardinality

FreeMonoid

Basic

Count

Symbols

GCDMonoid

Basic

Finset

IntegrallyClosed

Multiset

Nat

Group

Action

Basic

Defs

End

Faithful

Opposite

Option

Pi

Pretransitive

Prod

Sigma

Sum

TypeTags

Units

Commute

Basic

Defs

Hom

Units

Equiv

Basic

TypeTags

Fin

Basic

Tuple

Hom

Basic

CompTypeclasses

Defs

End

Instances

Invertible

Basic

Defs

Nat

Basic

Even

TypeTags

Units

Pi

Basic

Lemmas

Pointwise

Finset

Basic

Interval

Set

Basic

BigOperators

Card

Finite

ListOfFn

Semiconj

Basic

Defs

Units

Subgroup

ZPowers

Basic

Lemmas

Actions

Basic

Defs

Finite

Ker

Lattice

Map

MulOpposite

MulOppositeLemmas

Order

Pointwise

Submonoid

Basic

BigOperators

Defs

DistribMulAction

Membership

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

Aut

Basic

Center

Commutator

Conj

ConjFinite

Defs

Embedding

Even

EvenFunction

Ext

FiniteSupport

ForwardDiff

Graph

Indicator

InjSurj

Int

MinimalAxioms

NatPowAssoc

Operations

Opposite

PNatPowAssoc

Prod

Support

Translate

ULift

ZeroOne

GroupPower

IterateHom

GroupWithZero

Action

Basic

Defs

End

Faithful

Opposite

Pi

Prod

Units

Pointwise

Set

Basic

Card

Finset

Units

Basic

Equiv

Lemmas

Basic

Center

Commute

Conj

Defs

Divisibility

Hom

Indicator

InjSurj

Invertible

Nat

NeZero

NonZeroDivisors

Opposite

Pi

Prod

Semiconj

ULift

WithZero

Homology

DerivedCategory

Ext

Basic

ExactSequences

ExtClass

Basic

ExactFunctor

HomologySequence

ShortExact

SingleTriangle

Embedding

Basic

Boundary

Extend

ExtendHomology

HomEquiv

IsSupported

Restriction

StupidTrunc

TruncGE

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

RightHomology

ShortExact

SnakeLemma

Additive

Augment

Bifunctor

BifunctorAssociator

BifunctorFlip

BifunctorHomotopy

BifunctorShift

CommSq

ComplexShape

ComplexShapeSigns

ConcreteCategory

DifferentialObject

ExactSequence

Functor

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

Weights

Basic

Cartan

Chain

Killing

Linear

RootSystem

Abelian

BaseChange

Basic

CartanExists

CartanMatrix

CartanSubalgebra

Character

Classical

DirectSum

Engel

EngelSubalgebra

Free

IdealOperations

InvariantForm

Killing

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

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

MinimalAxioms

NatInt

Opposite

PID

Pi

PointwisePi

Prod

Projective

Rat

RingHom

SnakeLemma

Torsion

ULift

ZMod

MonoidAlgebra

Basic

Defs

Degree

Division

Grading

Ideal

NoZeroDivisors

Support

ToDirectSum

MvPolynomial

Basic

Cardinal

Comap

CommRing

Counit

Degrees

Derivation

Division

Equiv

Expand

Funext

Invertible

Monad

PDeriv

Polynomial

Rename

SchwartzZippel

Supported

Variables

NoZeroSMulDivisors

Basic

Defs

Pi

Prod

Order

Antidiag

Finsupp

Nat

Pi

Prod

Archimedean

Basic

Hom

Submonoid

BigOperators

Group

Finset

List

LocallyFinite

Multiset

GroupWithZero

List

Multiset

Ring

Finset

List

Multiset

Expect

CauSeq

Basic

BigOperators

Completion

Field

Canonical

Basic

Defs

Basic

Defs

InjSurj

Pi

Pointwise

Power

Rat

Subfield

Floor (file)

Div

Prime

Group

Action (file)

Synonym

Pointwise

Bounds

CompleteLattice

Interval

Unbundled

Abs

Basic

Int

Abs

Basic

Bounds

CompleteLattice

Cone

Defs

DenselyOrdered

Finset

Indicator

InjSurj

Instances

Int

Lattice

MinMax

Nat

Opposite

OrderIso

PiLex

PosPart

Prod

Synonym

TypeTags

Units

GroupWithZero

Action

Synonym

Unbundled (file)

Lemmas

Canonical

Finset

Submonoid

Synonym

WithZero

Hom

Basic

Monoid

Ring

Interval

Set

Group

Instances

Monoid

Basic

Finset

Multiset

Module

Algebra

Defs

OrderedSMul

Pointwise

Rat

Synonym

Monoid

Canonical

Basic

Defs

Unbundled

Basic

Defs

ExistsOfLE

MinMax

OrderDual

Pow

TypeTags

WithTop

Basic

Defs

NatCast

OrderDual

Prod

Submonoid

ToMulBot

TypeTags

Units

WithTop

Nonneg

Field

Floor

Module

Ring

Positive

Field

Ring

Ring

Unbundled

Basic

Nonneg

Rat

Abs

Basic

Canonical

Cast

Cone

Defs

Finset

InjSurj

Int

Nat

Opposite

Pow

Prod

Rat

Star

Synonym

WithTop

Star

Basic

Conjneg

Prod

Sub

Unbundled

Basic

Hom

Basic

Defs

Prod

WithTop

SuccPred (file)

TypeTags

WithBot

AbsoluteValue

AddGroupWithTop

AddTorsor

Algebra

Chebyshev

CompleteField

EuclideanAbsoluteValue

Invertible

Kleene

Monovary

Pi

Quantale

Rearrangement

Sum

ToIntervalMod

UpperLower

ZeroLEOne

PUnitInstances

Algebra

GCDMonoid

Module

Order

Pointwise

Stabilizer

Polynomial

Degree

CardPowDegree

Definitions

Domain

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

CoeffMem

DenomsClearable

Derivation

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Mirror

Monic

Monomial

PartialFractions

Reverse

RingDivision

Roots

Smeval

SpecificDegree

Splits

SumIteratedDerivative

Taylor

UnitTrinomial

PresentedMonoid

Basic

Prime

Defs

Lemmas

Regular

Basic

Pow

SMul

Ring

Action

Basic

Field

Group

Invariant

Subobjects

Divisibility

Basic

Lemmas

Hom

Basic

Defs

Int

Defs

Parity

Units

Pointwise

Finset

Set

Semireal

Defs

Subring

Basic

Defs

IntPolynomial

MulOpposite

Order

Pointwise

Units

Subsemiring

Basic

Defs

MulOpposite

Order

Pointwise

AddAut

Aut

Basic

BooleanRing

Center

Centralizer

CentroidHom

Commute

CompTypeclasses

Defs

Equiv

Ext

Fin

Idempotents

Identities

InjSurj

Invertible

MinimalAxioms

Nat

NegOnePow

Opposite

Parity

Pi

Prod

Rat

Regular

Semiconj

SumsOfSquares

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

StarRingHom

Subalgebra

Subsemiring

Unitary

Tropical

Basic

BigOperators

Lattice

Vertex

HVertexOperator

VertexOperator

AddTorsor

AlgebraicCard

CubicDiscriminant

DirectLimit

DualNumber

DualQuaternion

Exact

Expr

Free

FreeNonUnitalNonAssocAlgebra

GeomSum

GradedMonoid

GradedMulAction

HierarchyDesign

IsPrimePow

LinearRecurrence

ModEq

NeZero

Notation

Opposites

PEmptyInstances

Periodic

QuadraticDiscriminant

Quandle

Quaternion

QuaternionBasis

Quotient

RingQuot

SMulWithZero

Symmetrized

TrivSqZeroExt

AlgebraicGeometry

Cover

MorphismProperty

Open

Over

EllipticCurve

DivisionPolynomial

Basic

Degree

Affine

Group

IsomOfJ

Jacobian

ModelsWithJ

NormalForms

Projective

VariableChange

Weierstrass

Modules

Presheaf

Sheaf

Tilde

Morphisms

Affine

AffineAnd

Basic

ClosedImmersion

Constructors

Etale

Finite

FinitePresentation

FiniteType

Immersion

Integral

IsIso

OpenImmersion

Preimmersion

Proper

QuasiCompact

QuasiSeparated

RingHomProperties

Separated

Smooth

SurjectiveOnStalks

UnderlyingMap

UniversallyClosed

UniversallyInjective

PrimeSpectrum

Basic

FreeLocus

IsOpenComapC

Jacobson

Maximal

Module

Noetherian

TensorProduct

ProjectiveSpectrum

Basic

Proper

Scheme

StructureSheaf

Topology

Sites

BigZariski

Etale

MorphismProperty

Small

AffineScheme

AffineSpace

FunctionField

GammaSpecAdjunction

Gluing

GluingOneHypercover

Limits

Noetherian

OpenImmersion

Over

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

Quasicategory

Basic

Nerve

StrictSegal

SimplicialCategory

Basic

SimplicialObject

SimplicialObject

Basic

Coskeletal

SimplicialSet

Basic

Coskeletal

HomotopyCat

KanComplex

Monoidal

Nerve

Path

StrictSegal

AlternatingFaceMapComplex

CechNerve

ExtraDegeneracy

MooreComplex

SimplexCategory

SimplicialNerve

SingularSet

SplitSimplicialObject

TopologicalSimplex

Analysis

Analytic

Basic

CPolynomial

ChangeOrigin

Composition

Constructions

Inverse

IsolatedZeros

IteratedFDeriv

Linear

Meromorphic

OfScalars

Polynomial

RadiusLiminf

Uniqueness

Within

Asymptotics

AsymptoticEquivalent

Asymptotics

SpecificAsymptotics

SuperpolynomialDecay

TVS

Theta

BoxIntegral

Box

Basic

SubboxInduction

Partition

Additive

Basic

Filter

Measure

Split

SubboxInduction

Tagged

Basic

DivergenceTheorem

Integrability

UnitPartition

CStarAlgebra

ContinuousFunctionalCalculus

Basic

Instances

Integral

Isometric

NonUnital

Order

Restrict

Unique

Unital

Unitary

Module

Constructions

Defs

Synonym

SpecialFunctions

PosPart

ApproximateUnit

Basic

Classes

ContinuousLinearMap

ContinuousMap

Exponential

GelfandDuality

Hom

Matrix

Multiplier

Spectrum

Unitization

lpSpace

Calculus

AddTorsor

AffineMap

Coord

BumpFunction

Basic

Convolution

FiniteDimension

InnerProduct

Normed

Conformal

InnerProduct

NormedSpace

ContDiff

Basic

Bounds

CPolynomial

Defs

FTaylorSeries

FaaDiBruno

FiniteDimension

RCLike

WithLp

Deriv

Abs

Add

AffineMap

Basic

Comp

Inv

Inverse

Linear

Mul

Pi

Polynomial

Pow

Prod

Shift

Slope

Star

Support

ZPow

FDeriv

Add

Analytic

Basic

Bilinear

Comp

Equiv

Extend

Linear

Measurable

Mul

Norm

Pi

Prod

RestrictScalars

Star

Symmetric

WithLp

Gradient

Basic

InverseFunctionTheorem

ApproximatesLinearOn

ContDiff

Deriv

FDeriv

FiniteDimensional

IteratedDeriv

Defs

Lemmas

LineDeriv

Basic

IntegrationByParts

Measurable

QuadraticMap

LocalExtr

Basic

LineDeriv

Polynomial

Rolle

DSlope

Darboux

DiffContOnCl

FirstDerivativeTest

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

Topology

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

Extension

InnerDual

Pointed

Proper

SimplicialComplex

Basic

SpecificFunctions

Basic

Deriv

Pow

AmpleSet

Basic

Between

Birkhoff

Body

Caratheodory

Combination

Continuous

Contractible

Deriv

EGauge

Exposed

Extrema

Extreme

Function

Gauge

GaugeRescale

Hull

Independent

Integral

Intrinsic

Jensen

Join

KreinMilman

Measure

Mul

Normed

PartitionOfUnity

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

FourierTransform

FourierTransformDeriv

Inversion

PoissonSummation

RiemannLebesgueLemma

ZMod

FunctionalSpaces

SobolevInequality

InnerProductSpace

Adjoint

Basic

Calculus

Completion

ConformalLinearMap

Defs

Dual

EuclideanDist

GramSchmidtOrtho

JointEigenspace

LaxMilgram

LinearMap

LinearPMap

MeanErgodic

NormPow

OfNorm

Orientation

Orthogonal

Orthonormal

PiL2

Positive

ProdL2

Projection

Rayleigh

Semisimple

Spectrum

StarOrder

Subspace

Symmetric

TwoDim

WeakOperatorTopology

l2Space

LocallyConvex

AbsConvex

BalancedCoreHull

Barrelled

Basic

Bounded

ContinuousOfBounded

Polar

StrongTopology

WeakDual

WeakOperatorTopology

WeakSpace

WithSeminorms

Normed

Affine

AddTorsor

AddTorsorBases

ContinuousAffineMap

Isometry

MazurUlam

Algebra

Basic

Exponential

MatrixExponential

Norm

QuaternionExponential

Spectrum

TrivSqZeroExt

Ultra

Unitization

UnitizationL1

Field

Basic

InfiniteSum

Lemmas

ProperSpace

Ultra

UnitBall

Group

SemiNormedGrp (file)

Completion

Kernels

AddCircle

AddTorsor

BallSphere

Basic

Bounded

CocompactMap

Completeness

Completion

Constructions

ControlledClosure

Hom

HomCompletion

InfiniteSum

Int

Lemmas

NullSubmodule

Pointwise

Quotient

Rat

Seminorm

Submodule

Tannery

Ultra

Uniform

ZeroAtInfty

Lp

LpEquiv

PiLp

ProdLp

WithLp

lpSpace

Module

Basic

Complemented

Completion

Dual

FiniteDimension

Ray

Span

WeakDual

Operator

Banach

BanachSteinhaus

BoundedLinearMaps

Compact

ContinuousLinearMap

LinearIsometry

Order

Hom

Basic

Ultra

Basic

Lattice

UpperLower

Ring

IsPowMulFaithful

Seminorm

SeminormFromBounded

SeminormFromConst

Ultra

Units

WithAbs

MulAction

NormedSpace

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

Pointwise

RCLike

Real

RieszLemma

SphereNormEquiv

ODE

Gronwall

PicardLindelof

Polynomial

Basic

CauchyBound

RCLike

Basic

Inner

Lemmas

SpecialFunctions

Complex

Analytic

Arctan

Arg

Circle

CircleAddChar

Log

LogBounds

LogDeriv

ContinuousFunctionalCalculus

ExpLog

PosPart

Rpow

Gamma

Basic

Beta

BohrMollerup

Deligne

Deriv

Gaussian

FourierTransform

GaussianIntegral

PoissonSummation

Log

Base

Basic

Deriv

ENNRealLog

ENNRealLogExp

ERealExp

Monotone

NegMulLog

Pow

Asymptotics

Complex

Continuity

Deriv

Integral

NNReal

Real

Trigonometric

Angle

Arctan

ArctanDeriv

Basic

Bounds

Chebyshev

Complex

ComplexDeriv

Cotangent

Deriv

EulerSineProd

Inverse

InverseDeriv

Series

Arsinh

Bernstein

BinaryEntropy

CompareExp

Exp

ExpDeriv

Exponential

ImproperIntegrals

Integrals

JapaneseBracket

NonIntegrable

OrdinaryHypergeometric

PolarCoord

PolynomialExp

SmoothTransition

Sqrt

Stirling

SpecificLimits

Basic

FloorPow

Normed

RCLike

VonNeumannAlgebra

Basic

BoundedVariation

ConstantSpeed

Convolution

Hofer

Matrix

MeanInequalities

MeanInequalitiesPow

MellinInversion

MellinTransform

Oscillation

PSeries

PSeriesComplex

Quaternion

Seminorm

Subadditive

SumIntegralComparisons

SumOverResidueClass

CategoryTheory

Abelian

DiagramLemmas

Four

GrothendieckAxioms

Basic

FunctorCategory

Sheaf

Basic

EpiWithInjectiveKernel

Exact

Ext

FunctorCategory

Generator

GrothendieckCategory

Images

Injective

InjectiveResolution

LeftDerived

NonPreadditive

Opposite

Projective

ProjectiveResolution

Pseudoelements

Refinements

RightDerived

Subobject

Transfer

Action (file)

Basic

Concrete

Continuous

Limits

Monoidal

Adjunction

Lifting

Left

Right

AdjointFunctorTheorems

Basic

Comma

Evaluation

FullyFaithful

Limits

Mates

Opposites

Over

PartialAdjoint

Reflective

Restrict

Triple

Unique

Whiskering

Bicategory

Functor

Lax

LocallyDiscrete

Oplax

Prelax

Pseudofunctor

FunctorBicategory

Oplax

Kan

Adjunction

HasKan

IsKan

Modification

Oplax

NaturalTransformation

Oplax

Strong

Adjunction

Basic

Coherence

End

Extension

Free

Grothendieck

LocallyDiscrete

SingleObj

Strict

Category

Cat (file)

Adjunction

AsSmall

Limit

Basic

Bipointed

Factorisation

GaloisConnection

Grpd

Init

KleisliCat

Pairwise

PartialFun

Pointed

Preorder

Quiv

ReflQuiv

RelCat

TwoP

ULift

ChosenFiniteProducts (file)

Cat

FunctorCategory

Closed

FunctorCategory

Complete

Groupoid

Cartesian

Enrichment

Functor

FunctorToTypes

Ideal

Monoidal

Types

Zero

Comma

Presheaf

Basic

Colimit

StructuredArrow

Basic

Functor

Small

Arrow

Basic

Final

Over

OverClass

ConcreteCategory

Basic

Bundled

BundledHom

Elementwise

EpiMono

ReflectsIso

UnbundledHom

Dialectica

Basic

Monoidal

EffectiveEpi

Basic

Comp

Coproduct

Enough

Extensive

Preserves

RegularEpi

Endofunctor

Algebra

Enriched

Basic

FunctorCategory

HomCongr

Opposite

Ordinary

FiberedCategory

BasedCategory

Cartesian

Cocartesian

Fiber

Fibered

HomLift

Filtered

Basic

Connected

Final

Grothendieck

OfColimitCommutesFiniteLimit

Small

FinCategory

AsType

Basic

Functor

Derived

RightDerived

KanExtension

Adjunction

Basic

Pointwise

Basic

Category

Const

Currying

EpiMono

Flat

FullyFaithful

FunctorHom

Functorial

Hom

OfSequence

ReflectsIso

Trifunctor

Galois

Action

Basic

Decomposition

EssSurj

Examples

Full

GaloisObjects

IsFundamentalgroup

Prorepresentability

Topology

GradedObject (file)

Associator

Bifunctor

Braiding

Monoidal

Single

Trifunctor

Unitor

Groupoid (file)

Basic

Discrete

FreeGroupoid

Subgroupoid

VertexGroup

GuitartExact

Basic

VerticalComposition

Idempotents

Basic

Biproducts

FunctorCategories

FunctorExtension

HomologicalComplex

Karoubi

KaroubiKaroubi

SimplicialObject

LiftingProperties

Adjunction

Basic

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

Basic

EpiMono

Filtered

Finite

Indization

Category

Equalizers

FilteredColimits

IndObject

LocallySmall

Products

Preserves

Shapes

BinaryProducts

Biproducts

Equalizers

Images

Kernels

Products

Pullbacks

Square

Terminal

Zero

Basic

Filtered

Finite

FunctorCategory

Limits

Opposites

Presheaf

Ulift

Yoneda

Shapes

NormalMono

Basic

Equalizers

Pullback

Assoc

CommSq

Cospan

Equalizer

HasPullback

Iso

Mono

Pasting

PullbackCone

Square

BinaryProducts

Biproducts

CombinedProducts

ConcreteCategory

Connected

Countable

Diagonal

DisjointCoproduct

End

Equalizers

Equivalence

FiniteLimits

FiniteProducts

FunctorToTypes

Grothendieck

Images

IsTerminal

KernelPair

Kernels

Multiequalizer

PiProd

Products

Reflexive

RegularMono

SequentialProduct

SingleObj

SplitCoequalizer

SplitEqualizer

StrictInitial

StrongEpi

Terminal

Types

WideEqualizers

WidePullbacks

ZeroMorphisms

ZeroObjects

Bicones

ColimitLimit

Comma

ConeCategory

Cones

Connected

Creates

Elements

EpiMono

EssentiallySmall

ExactFunctor

Filtered

FilteredColimitCommutesFiniteLimit

FilteredColimitCommutesProduct

FinallySmall

FintypeCat

Fubini

FullSubcategory

FunctorToTypes

HasLimits

IndYoneda

IsConnected

IsLimit

Lattice

MonoCoprod

MorphismProperty

Opposites

Over

Pi

Presheaf

Sifted

SmallComplete

Types

TypesFiltered

Unit

VanKampen

Yoneda

Linear

Basic

FunctorCategory

LinearFunctor

Yoneda

Localization

CalculusOfFractions (file)

ComposableArrows

Fractions

Preadditive

DerivabilityStructure

Basic

Constructor

Adjunction

Bifunctor

Bousfield

Composition

Construction

Equivalence

FiniteProducts

HasLocalization

HomEquiv

LocalizerMorphism

Opposite

Pi

Predicate

Prod

Resolution

SmallHom

SmallShiftedHom

StructuredArrow

Triangulated

Monad

Adjunction

Algebra

Basic

Coequalizer

Comonadicity

Equalizer

EquivMon

Kleisli

Limits

Monadicity

Products

Types

Monoidal

Braided

Basic

Opposite

Reflection

Cartesian

Comon_

Free

Basic

Coherence

Internal

FunctorCategory

Limits

Module

Types

OfChosenFiniteProducts

Basic

Symmetric

Rigid

Basic

Braided

FunctorCategory

OfEquivalence

Types

Basic

Coyoneda

Symmetric

Bimod

Bimon_

Category

Center

CoherenceLemmas

CommMon_

Comon_

Conv

Discrete

End

Functor

FunctorCategory

Hopf_

Limits

Linear

Mod_

Mon_

NaturalTransformation

OfHasFiniteProducts

Opposite

Preadditive

Skeleton

Subcategory

Tor

Transport

MorphismProperty

Basic

Comma

Composition

Concrete

Factorization

IsInvertedBy

Limits

OverAdjunction

Representable

Retract

TransfiniteComposition

PathCategory

Basic

MorphismProperty

Pi

Basic

Preadditive

Yoneda

Basic

Injective

Limits

Projective

AdditiveFunctor

Basic

Biproducts

EilenbergMoore

EndoFunctor

FunctorCategory

Generator

HomOrthogonal

Injective

InjectiveResolution

LeftExact

Mat

OfBiproducts

Opposite

Projective

ProjectiveResolution

Schur

SingleObj

Products

Associator

Basic

Bifunctor

Unitor

Quotient (file)

Linear

Preadditive

Shift

Adjunction

Basic

CommShift

Induced

InducedShiftSequence

Localization

Opposite

Predicate

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

ChosenFiniteProducts

Closed

CompatiblePlus

CompatibleSheafification

ConcreteSheafification

ConstantSheaf

Continuous

CoverLifting

CoverPreserving

Coverage

CoversTop

EffectiveEpimorphic

EpiMono

EqualizerSheafCondition

Equivalence

Grothendieck

IsSheafFor

IsSheafOneHypercover

LeftExact

Limits

Localization

LocallyBijective

LocallyFullyFaithful

LocallyInjective

LocallySurjective

MayerVietorisSquare

MorphismProperty

OneHypercover

Over

Plus

Preserves

PreservesLocallyBijective

PreservesSheafification

Pretopology

Pullback

Sheaf

SheafHom

SheafOfTypes

Sheafification

Sieves

Spaces

Subcanonical

Subsheaf

Types

Whiskering

SmallObject

Iteration

Basic

ExtendToSucc

Nonempty

UniqueHom

Construction

TransfiniteCompositionLifting

WellOrderInductionData

Subobject

Basic

Comma

FactorThru

Lattice

Limits

MonoOver

Types

WellPowered

Sums

Associator

Basic

Triangulated

TStructure

Basic

Basic

Functor

HomologicalFunctor

Opposite

Pretriangulated

Rotate

Subcategory

TriangleShift

Triangulated

Yoneda

Adhesive

Balanced

CatCommSq

ClosedUnderIsomorphisms

CodiscreteCategory

CofilteredSystem

CommSq

ComposableArrows

Conj

ConnectedComponents

Core

Countable

DifferentialObject

DiscreteCategory

Elements

Elementwise

Endomorphism

EpiMono

EqToHom

Equivalence

EssentialImage

EssentiallySmall

Extensive

FintypeCat

FullSubcategory

Generator

GlueData

Grothendieck

HomCongr

IsConnected

Iso

IsomorphismClasses

NatIso

NatTrans

Noetherian

Opposites

PEmpty

PUnit

Retract

Simple

SingleObj

Skeletal

Square

Subterminal

Thin

Types

UnivLE

Whiskering

Widesubcategory

WithTerminal

Yoneda

Combinatorics

Additive

AP

Three

Behrend

Defs

Corner

Defs

Roth

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

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

Subgraph

WalkCounting

Ends

Defs

Properties

Regularity

Bound

Chunk

Energy

Equitabilise

Increment

Lemma

Uniform

Triangle

Basic

Counting

Removal

Tripartite

Acyclic

AdjMatrix

Basic

Circulant

Clique

Coloring

ConcreteColorings

Dart

DegreeSum

Density

Diam

Finite

Finsubgraph

Girth

Hamiltonian

Hasse

IncMatrix

Init

LapMatrix

LineGraph

Maps

Matching

Metric

Operations

Partition

Path

Prod

StronglyRegular

Subgraph

Sum

Trails

Turan

UniversalVerts

Walk

Young

SemistandardTableau

YoungDiagram

Colex

Configuration

HalesJewett

Hindman

Pigeonhole

Schnirelmann

Computability

AkraBazzi

AkraBazzi

GrowsPolynomially

Ackermann

ContextFreeGrammar

DFA

Encoding

EpsilonNFA

Halting

Language

NFA

Partrec

PartrecCode

Primrec

Reduce

RegularExpressions

TMComputable

TMToPartrec

TuringMachine

Condensed

Discrete

Basic

Characterization

Colimit

LocallyConstant

Module

Light

AB

Basic

CartesianClosed

Epi

Explicit

Functors

Limits

Module

TopCatAdjunction

TopComparison

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

ExtractLemmas

Lemmas

Bool

AllAny

Basic

Count

Set

Complex

Abs

Basic

BigOperators

Cardinality

Determinant

Exponential

ExponentialBounds

FiniteDimensional

Module

Order

Orientation

Countable

Basic

Defs

Small

DFinsupp

BigOperators

Defs

Encodable

Ext

FiniteInfinite

Interval

Lex

Module

Multiset

NeLocus

Notation

Order

Sigma

Submonoid

WellFounded

DList

Instances

ENNReal

Basic

Inv

Lemmas

Operations

Real

ENat

Basic

BigOperators

Defs

Lattice

FP

Basic

Fin

Tuple

Basic

BubbleSortInduction

Curry

Finset

NatAntidiagonal

Reflection

Sort

Take

Basic

Fin2

FlagRange

Parity

SuccPred

VecNotation

FinEnum (file)

Option

Finite

Card

Defs

Powerset

Prod

Set

Sigma

Sum

Vector

Finset

Lattice

Basic

Fold

Lemmas

Attach

Attr

Basic

Card

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

Fin

Fintype

Indicator

Interval

Lex

Multiset

NeLocus

Notation

Order

PWO

Pointwise

SMulWithZero

ToDFinsupp

Weight

WellFounded

Fintype

Basic

BigOperators

Card

CardEmbedding

Fin

Lattice

List

Option

Order

Parity

Perm

Pi

Powerset

Prod

Quotient

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

Bitwise

CardIntervalMod

CharZero

ConditionallyCompleteOrder

Defs

DivMod

GCD

Interval

LeastGreatest

Lemmas

Log

ModEq

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

Infix

InsertIdx

InsertNth

Intervals

Iterate

Lattice

Lemmas

Lex

MinMax

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

Pairwise

Palindrome

Permutation

Pi

Prime

ProdSigma

Range

ReduceOption

Rotate

Sections

Sigma

Sort

SplitBy

SplitLengths

Sublists

Sym

TFAE

ToFinsupp

Zip

MLList

BestFirst

Dedup

DepthFirst

IO

Split

Matrix

Auto

Basic

Basis

Bilinear

Block

CharP

ColumnRowPartitioned

Composition

ConjTranspose

DMatrix

Defs

Diagonal

DoublyStochastic

DualNumber

Hadamard

Invertible

Kronecker

Mul

Notation

PEquiv

Rank

Reflection

RowCol

Matroid

Basic

Closure

Constructions

Dual

IndepAxioms

Init

Map

Restrict

Sum

Multiset

Antidiagonal

Basic

Bind

Dedup

FinsetOps

Fintype

Fold

Functor

Interval

Lattice

NatAntidiagonal

Nodup

OrderedMonoid

Pi

Powerset

Range

Sections

Sort

Sum

Sym

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

Factorial

Basic

BigOperators

Cast

DoubleFactorial

SuperFactorial

Factorization

Basic

Defs

Induction

PrimePow

Root

Fib

Basic

Zeckendorf

GCD

Basic

BigOperators

Order

Lemmas

Prime

Basic

Defs

Factorial

Infinite

Int

Nth

Pow

BinaryRec

BitIndices

Bits

Bitwise

ChineseRemainder

Count

Defs

Digits

Dist

EvenOddRec

Factors

Find

Hyperoperation

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

Option

Basic

Defs

NAry

Ordering

Basic

Lemmas

Ordmap

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

ConjExponents

ENatENNReal

EReal

GoldenRatio

Hyperreal

Irrational

IsNonarchimedean

Pointwise

Sign

Sqrt

Star

StarOrdered

Seq

Computation

Parallel

Seq

WSeq

Set

Finite

Basic

Lattice

Lemmas

List

Monad

Powerset

Range

Pairwise

Basic

Lattice

Pointwise

Iterate

SMul

Support

Accumulate

Basic

BoolIndicator

Card

Constructions

Countable

Defs

Enumerate

Equitable

Function

Functor

Image

Lattice

List

MemPartition

Monotone

MulAntidiagonal

NAry

Notation

Operations

Opposite

Prod

SMulAntidiagonal

Semiring

Sigma

Subset

Subsingleton

Sups

SymmDiff

UnionLift

SetLike

Basic

Fintype

Setoid

Basic

Partition

Sigma

Basic

Interval

Lex

Order

Stream

Defs

Init

String

Basic

Defs

Lemmas

Sum

Basic

Interval

Lattice

Order

Sym

Sym2 (file)

Init

Order

Basic

Card

Tree

Basic

Get

RBMap

Vector

Basic

Defs

MapLemmas

Mem

Snoc

Zip

W

Basic

Cardinal

Constructions

ZMod

Aut

Basic

Coprime

Defs

Factorial

IntUnitsPower

Quotient

Units

BitVec

Bracket

Bundle

Char

Erased

Finmap

Holor

Ineq

Opposite

PEquiv

PFun

Part

Quot

Rel

SProd

Semiquot

Sign

Subtype

TwoPointing

TypeMax

TypeVec

UInt

ULift

Vector3

Deprecated

Cardinal

Continuum

Finite

PartENat

AlgebraClasses

Aliases

ByteArray

Combinator

Equiv

Group

HashMap

LazyList

Logic

MinMax

NatLemmas

Order

RelClasses

Ring

Subfield

Subgroup

Submonoid

Subring

Dynamics

BirkhoffSum

Average

Basic

NormedSpace

Circle

RotationNumber

TranslationNumber

Ergodic

Action

Basic

OfMinimal

Regular

AddCircle

Conservative

Ergodic

Function

MeasurePreserving

FixedPoints

Basic

Topology

TopologicalEntropy

CoverEntropy

DynamicalEntourage

NetEntropy

Semiconj

Flow

Minimal

Newton

OmegaLimit

PeriodicPts

FieldTheory

Differential

Basic

Finite

Basic

GaloisField

Polynomial

Trace

Galois

Basic

GaloisClosure

Infinite

Profinite

IntermediateField

Algebraic

Basic

IsAlgClosed

AlgebraicClosure

Basic

Classification

Spectrum

Minpoly

Basic

Field

IsConjRoot

IsIntegrallyClosed

MinpolyDiv

MvRatFunc

Rank

RatFunc

AsPolynomial

Basic

Defs

Degree

SplittingField

Construction

IsSplittingField

AbelRuffini

AbsoluteGaloisGroup

Adjoin

AlgebraicClosure

AxGrothendieck

CardinalEmb

Cardinality

ChevalleyWarning

Extension

Finiteness

Fixed

IsPerfectClosure

IsSepClosed

Isaacs

JacobsonNoether

KrullTopology

KummerExtension

Laurent

LinearDisjoint

Normal

NormalClosure

Perfect

PerfectClosure

PolynomialGaloisGroup

PrimitiveElement

PurelyInseparable

Relrank

Separable

SeparableClosure

SeparableDegree

Tower

Geometry

Euclidean

Angle

Oriented

Affine

Basic

RightAngle

Rotation

Unoriented

Affine

Basic

Conformal

RightAngle

Sphere

Inversion

Basic

Calculus

ImageHyperplane

Sphere

Basic

Power

Ptolemy

SecondInter

Basic

Circumcenter

MongePoint

PerpBisector

Triangle

Group

Growth

QuotientInter

Manifold

Algebra

LeftInvariantDerivation

LieGroup

Monoid

SmoothFunctions

Structures

ContMDiff

Atlas

Basic

Defs

NormedSpace

Product

Instances

Real

Sphere

UnitsOfNormedAlgebra

IntegralCurve

Basic

ExistUnique

Transform

UniformTime

MFDeriv

Atlas

Basic

Defs

FDeriv

NormedSpace

SpecificFunctions

Tangent

UniqueDifferential

Sheaf

Basic

LocallyRingedSpace

Smooth

VectorBundle

Basic

FiberwiseLinear

Hom

MDifferentiable

Pullback

SmoothSection

Tangent

AnalyticManifold

BumpFunction

ChartedSpace

Complex

ConformalGroupoid

ContMDiffMFDeriv

ContMDiffMap

DerivationBundle

Diffeomorph

InteriorBoundary

LocalDiffeomorph

LocalInvariantProperties

Metrizable

PartitionOfUnity

PoincareConjecture

SmoothManifoldWithCorners

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

IsFreeGroup

NielsenSchreier

Reduce

GroupAction

DomAct

ActionHom

Basic

SubMulAction (file)

Pointwise

Basic

Blocks

CardCommute

ConjAct

Defs

Embedding

FixedPoints

FixingSubgroup

Hom

IterateAct

Period

Pointwise

Quotient

Ring

Support

GroupExtension

Defs

MonoidLocalization

Away

Basic

Cardinality

MonoidWithZero

Order

Order

Min

OreLocalization

Basic

Cardinality

OreSet

Perm

Cycle

Basic

Concrete

Factors

PossibleTypes

Type

Basic

Closure

ClosureSwap

ConjAct

DomMulAct

Fin

Finite

List

Option

Sign

Subgroup

Support

ViaEmbedding

QuotientGroup

Basic

Defs

Finite

SpecificGroups

Alternating

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

FreeAbelianGroupFinsupp

Goursat

HNNExtension

Index

Nilpotent

NoncommCoprod

NoncommPiCoprod

OrderOfElement

PGroup

PresentedGroup

PushoutI

Schreier

SchurZassenhaus

SemidirectProduct

Solvable

Sylow

Torsion

Transfer

InformationTheory

Hamming

Lean

Elab

Tactic

Basic

Term

Expr (file)

Basic

ExtraRecognizers

Rat

ReplaceRec

Meta (file)

Basic

CongrTheorems

DiscrTree

KAbstractPositions

Simp

PrettyPrinter

Delaborator

CoreM

EnvExtension

Exception

GoalsLocation

Json

LocalContext

Message

Name

Thunk

LinearAlgebra

AffineSpace

AffineEquiv

AffineMap

AffineSubspace

Basic

Basis

Combination

ContinuousAffineEquiv

FiniteDimensional

Independent

Matrix

Midpoint

MidpointZero

Ordered

Pointwise

Restrict

Slope

Alternating

Basic

DomCoprod

Basis

Basic

Bilinear

Cardinality

Defs

Flag

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

DirectSum

Finsupp

TensorProduct

Eigenspace

Basic

Matrix

Minpoly

Pi

Semisimple

Triangularizable

Zero

ExteriorAlgebra

Basic

Grading

OfAlternating

ExteriorPower

Basic

FiniteDimensional (file)

Defs

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

Matrix

Basic

Determinant

IdealQuotient

Int

Norm

PID

StrongRankCondition

FreeProduct

Basic

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

InvariantBasisNumber

IsDiag

LDL

MvPolynomial

Nondegenerate

NonsingularInverse

Orthogonal

Permanent

Permutation

Polynomial

PosDef

ProjectiveSpecialLinearGroup

Reindex

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

Spectrum

StdBasis

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

ZPow

Multilinear

Basic

Basis

DFinsupp

FiniteDimensional

Pi

TensorProduct

Projectivization

Basic

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

Nondegenerate

Basic

Defs

Hom

OfBilinear

RootPairingCat

RootPositive

WeylGroup

Span

Basic

Defs

TensorAlgebra

Basic

Basis

Grading

ToTensorPower

TensorProduct

Graded

External

Internal

Basic

Basis

DirectLimit

Finiteness

Matrix

Opposite

Pi

Prod

Quotient

RightExactness

Subalgebra

Submodule

Tower

Vanishing

AnnihilatingPolynomial

BilinearMap

Coevaluation

Contraction

Countable

CrossProduct

DFinsupp

Determinant

Dual

FiniteSpan

FreeAlgebra

GeneralLinearGroup

Goursat

InvariantBasisNumber

Isomorphisms

JordanChevalley

Lagrange

LinearDisjoint

LinearIndependent

LinearPMap

Orientation

PID

PerfectPairing

Pi

PiTensorProduct

Prod

Projection

Ray

Reflection

SModEq

Semisimple

SesquilinearForm

StdBasis

SymplecticGroup

TensorPower

Trace

UnitaryGroup

Vandermonde

Logic

Embedding

Basic

Set

Encodable

Basic

Lattice

Equiv

Array

Basic

Defs

Embedding

Fin

Fintype

Functor

List

Nat

Option

Pairwise

PartialEquiv

Set

Function

Basic

CompTypeclasses

Conjugate

Defs

FiberPartition

FromTypes

Iterate

OfArity

ULift

Godel

GodelBetaFunction

Nontrivial

Basic

Defs

Small

Basic

Defs

Group

List

Module

Ring

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

AddChar

Cylinders

EventuallyMeasurable

HaarToSphere

Pi

Projective

SubmoduleQuotient

UnitInterval

Covering

Besicovitch

BesicovitchVectorSpace

DensityTheorem

Differentiation

LiminfLimsup

OneDim

Vitali

VitaliFamily

Decomposition

Exhaustion

Jordan

Lebesgue

RadonNikodym

SignedHahn

SignedLebesgue

UnsignedHahn

Function

AEEqFun (file)

DomAct

ConditionalExpectation

AEMeasurable

Basic

CondexpL1

CondexpL2

Indicator

Real

Unique

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

TriangleInequality

Trim

LpSpace (file)

DomAct

Basic

Continuous

ContinuousCompMeasurePreserving

SpecialFunctions

Arctan

Basic

Inner

RCLike

StronglyMeasurable

Basic

Inner

Lemmas

Lp

AEEqOfIntegral

AEMeasurableOrder

AEMeasurableSequence

ContinuousMapDense

ConvergenceInMeasure

Egorov

EssSup

Floor

Intersectivity

Jacobian

L1Space

L2Space

LocallyIntegrable

LpOrder

SimpleFunc

SimpleFuncDense

SimpleFuncDenseLp

UnifTight

UniformIntegrable

Group

AEStabilizer

Action

AddCircle

Arithmetic

Convolution

Defs

FundamentalDomain

GeometryOfNumbers

Integral

LIntegral

MeasurableEquiv

Measure

Pointwise

Prod

Integral

Asymptotics

Average

Bochner

BoundedContinuousFunction

CircleIntegral

CircleTransform

DivergenceTheorem

DominatedConvergence

ExpDecay

FundThmCalculus

Gamma

Indicator

IntegrableOn

IntegralEqImproper

IntervalAverage

IntervalIntegral

Layercake

Lebesgue

LebesgueNormedSpace

Marginal

MeanInequalities

PeakFunction

Periodic

Pi

Prod

RieszMarkovKakutani

SetIntegral

SetToL1

TorusIntegral

VitaliCaratheodory

MeasurableSpace

Basic

Card

CountablyGenerated

Defs

Embedding

Instances

Invariants

NCard

PreorderRestrict

Prod

Measure

Haar

Basic

Disintegration

InnerProductSpace

NormedSpace

OfBasis

Quotient

Unique

Lebesgue

Basic

Complex

EqHaar

Integral

VolumeOfBalls

AEDisjoint

AEMeasurable

AddContent

Comap

Complex

Content

ContinuousPreimage

Count

Dirac

DiracProba

Doubling

EverywherePos

FiniteMeasure

FiniteMeasureProd

GiryMonad

HasOuterApproxClosed

Hausdorff

LevyProkhorovMetric

LogLikelihoodRatio

MeasureSpace

MeasureSpaceDef

MutuallySingular

NullMeasurable

OpenPos

Portmanteau

ProbabilityMeasure

Prod

Regular

Restrict

SeparableMeasure

Stieltjes

Sub

Tilted

Trim

Typeclasses

WithDensity

WithDensityFinite

Order

Group

Lattice

Lattice

UpperLower

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfFunction

Operations

VectorMeasure

Basic

WithDensity

PiSystem

SetAlgebra

SetSemiring

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

Three

Harmonic

Bounds

Defs

EulerMascheroni

GammaDeriv

Int

ZetaAsymp

JacobiSum

Basic

LSeries

AbstractFuncEq

Basic

Convergence

Convolution

Deriv

Dirichlet

DirichletContinuation

HurwitzZeta

HurwitzZetaEven

HurwitzZetaOdd

HurwitzZetaValues

Linearity

MellinEqDirichlet

Nonvanishing

Positivity

PrimesInAP

RiemannZeta

ZMod

LegendreSymbol

QuadraticChar

Basic

GaussSum

AddCharacter

Basic

GaussEisensteinLemmas

JacobiSymbol

QuadraticReciprocity

ZModChar

ModularForms

EisensteinSeries

Basic

Defs

IsBoundedAtImInfty

MDifferentiable

UniformConvergence

JacobiTheta

Bounds

Manifold

OneVariable

TwoVariable

Basic

CongruenceSubgroups

Identities

LevelOne

QExpansion

SlashActions

SlashInvariantForms

MulChar

Basic

Duality

Lemmas

NumberField

CanonicalEmbedding

Basic

ConvexBody

FundamentalCone

Discriminant

Basic

Defs

Units

Basic

DirichletTheorem

Regulator

AdeleRing

Basic

ClassNumber

Completion

Embeddings

EquivReindex

FinitePlaces

FractionalIdeal

House

Norm

Padics

PadicVal

Basic

Defs

Hensel

MahlerBasis

PadicIntegers

PadicNorm

PadicNumbers

ProperSpace

RingHoms

RamificationInertia

Basic

Transcendental

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

SiegelsLemma

SmoothNumbers

SumFourSquares

SumPrimeReciprocals

SumTwoSquares

VonMangoldt

WellApproximable

Wilson

ZetaValues

Order

Atoms (file)

Finite

BoundedOrder

Basic

Lattice

Monotone

Bounds

Basic

Defs

Image

OrderIso

Category

BddDistLat

BddLat

BddOrd

BoolAlg

CompleteLat

DistLat

FinBddDistLat

FinBoolAlg

FinPartOrd

Frm

HeytAlg

Lat

LinOrd

NonemptyFinLinOrd

OmegaCompletePartialOrder

PartOrd

Preord

Semilat

CompactlyGenerated

Basic

Intervals

CompleteLattice (file)

Finset

ConditionallyCompleteLattice

Basic

Defs

Finset

Group

Indexed

Defs

LinearOrder

PartialOrder

Unbundled

Extension

Linear

Well

Filter

AtTopBot (file)

Archimedean

BigOperators

CountablyGenerated

Field

Floor

Group

ModEq

Monoid

Ring

Germ

Basic

OrderedMonoid

Bases

Basic

CardinalInter

Cocardinal

Cofinite

CountableInter

CountableSeparatingOn

CountablyGenerated

Curry

Defs

ENNReal

EventuallyConst

Extr

FilterProduct

Finite

IndicatorFunction

Interval

Ker

Lift

ListTraverse

NAry

Partial

Pi

Pointwise

Prod

Ring

SmallSets

Subsingleton

Tendsto

Ultrafilter

ZeroAndBoundedAtFilter

Fin

Basic

Tuple

Heyting

Basic

Boundary

Hom

Regular

Hom

Basic

Bounded

CompleteLattice

Lattice

Order

Set

Interval

Finset

Basic

Box

Defs

Fin

Nat

Set

Basic

Defs

Disjoint

Image

Infinite

IsoIoo

Monotone

OrdConnected

OrdConnectedComponent

OrderEmbedding

OrderIso

Pi

ProjIcc

SurjOn

UnorderedInterval

WithBotTop

Basic

Multiset

Monotone

Basic

Extension

Monovary

MonovaryOrder

Odd

Union

Partition

Equipartition

Finpartition

Rel

GaloisConnection

RelIso

Basic

Group

Set

SuccPred

Archimedean

Basic

CompleteLinearOrder

InitialSeg

IntervalSucc

Limit

LinearLocallyFinite

Relation

Tree

WithBot

UpperLower

Basic

Hom

LocallyFinite

Antichain

Antisymmetrization

Basic

Birkhoff

BooleanAlgebra

BooleanGenerators

BooleanSubalgebra

Booleanisation

Bounded

Chain

Circular

Closure

Cofinal

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

CompletePartialOrder

CompleteSublattice

Concept

Copy

CountableDenseLinearOrder

Cover

Directed

DirectedInverseSystem

Disjoint

Disjointed

Estimator

FixedPoints

GaloisConnection

GameAdd

Grade

Height

Ideal

InitialSeg

Irreducible

Iterate

JordanHolder

KonigLemma

KrullDimension

Lattice

LatticeIntervals

LiminfLimsup

Max

MinMax

Minimal

ModularLattice

Nat

Notation

OmegaCompletePartialOrder

OrdContinuous

OrderIsoNat

PFilter

Part

PartialSups

PiLex

PrimeIdeal

PrimeSeparator

PropInstances

Radical

RelClasses

RelSeries

Restriction

ScottContinuity

SemiconjSup

SetNotation

Sublattice

SupClosed

SupIndep

SymmDiff

Synonym

TypeTags

ULift

WellFounded

WellFoundedSet

WithBot

Zorn

ZornAtoms

Probability

Distributions

Exponential

Gamma

Gaussian

Geometric

Pareto

Poisson

Uniform

Independence

Basic

Conditional

Integrable

Kernel

ZeroOne

Kernel

Composition

Basic

IntegralCompProd

MeasureCompProd

ParallelComp

Disintegration

Basic

CDFToKernel

CondCDF

Density

Integral

MeasurableStieltjes

StandardBorel

Unique

Basic

CondDistrib

Condexp

Defs

Integral

Invariance

MeasurableIntegral

RadonNikodym

WithDensity

Martingale

Basic

BorelCantelli

Centering

Convergence

OptionalSampling

OptionalStopping

Upcrossing

ProbabilityMassFunction

Basic

Binomial

Constructions

Integrals

Monad

Process

Adapted

Filtration

HittingTime

PartitionFiltration

Stopping

BorelCantelli

CDF

ConditionalExpectation

ConditionalProbability

Density

IdentDistrib

Integration

Moments

Notation

StrongLaw

UniformOn

Variance

RepresentationTheory

GroupCohomology

Basic

Hilbert90

LowDegree

Resolution

Basic

Character

FDRep

Invariants

Maschke

Rep

RingTheory

AdicCompletion

Algebra

AsTensorProduct

Basic

Exactness

Functoriality

Adjoin

Basic

Dimension

FG

Field

Polynomial

PowerBasis

Tower

Algebraic

Basic

Cardinality

Defs

Integral

LinearIndependent

MvPolynomial

Pi

AlgebraicIndependent

Adjoin

AlgebraicClosure

Basic

Defs

RankAndCardinality

TranscendenceBasis

Transcendental

Bialgebra

Basic

Equiv

Hom

TensorProduct

Coalgebra

Basic

Equiv

Hom

TensorProduct

Congruence

Basic

BigOperators

Defs

Opposite

Coprime

Basic

Ideal

Lemmas

DedekindDomain

AdicValuation

Basic

Different

Dvr

Factorization

FiniteAdeleRing

Ideal

IntegralClosure

PID

SInteger

SelmerGroup

Derivation

Basic

DifferentialRing

Lie

MapCoeffs

ToSquareZero

DiscreteValuationRing

Basic

TFAE

DividedPowers

Basic

Etale

Basic

Field

Finiteness

Basic

Bilinear

Cardinality

Defs

Finsupp

Ideal

Lattice

Nakayama

Nilpotent

Prod

Projective

Subalgebra

TensorProduct

Flat

Basic

CategoryTheory

Equalizer

EquationalCriterion

FaithfullyFlat

Localization

Stability

FractionalIdeal

Basic

Extended

Norm

Operations

GradedAlgebra

Basic

HomogeneousIdeal

HomogeneousLocalization

Noetherian

Radical

HahnSeries

Addition

Basic

Multiplication

PowerSeries

Summable

Valuation

Ideal

Norm

AbsNorm

RelNorm

Quotient

Basic

Defs

Nilpotent

Noetherian

Operations

AssociatedPrime

Basic

Basis

BigOperators

Colon

Cotangent

Defs

IdempotentFG

IsPrimary

IsPrincipal

IsPrincipalPowQuotient

Lattice

Maps

Maximal

MinimalPrime

Nonunits

Operations

Over

Pointwise

Prime

Prod

Span

Int

Basic

IntegralClosure

Algebra

Basic

Defs

IsIntegral

Basic

Defs

IsIntegralClosure

Basic

Defs

IntegralRestrict

IntegrallyClosed

Jacobson

Ideal

Polynomial

Ring

Kaehler

Basic

CotangentComplex

Polynomial

TensorProduct

KrullDimension

Basic

Field

LocalProperties

Basic

Exactness

IntegrallyClosed

Projective

Reduced

Submodule

LocalRing

MaximalIdeal

Basic

Defs

ResidueField

Basic

Defs

Ideal

RingHom

Basic

Basic

Defs

Module

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

Submodule

MvPolynomial (file)

Symmetric

Defs

FundamentalTheorem

NewtonIdentities

Basic

EulerIdentity

FreeCommRing

Groebner

Homogeneous

Ideal

Localization

MonomialOrder

Tower

WeightedHomogeneous

MvPowerSeries

Basic

Inverse

LexOrder

NoZeroDivisors

Order

PiTopology

Trunc

Nilpotent

Basic

Defs

Lemmas

Noetherian

Basic

Defs

Filter

Nilpotent

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Basic

Defs

Transitivity

OreLocalization

Basic

Cardinality

OreSet

Ring

Polynomial

Cyclotomic

Basic

Eval

Expand

Roots

Eisenstein

Basic

IsIntegral

Hermite

Basic

Gaussian

Basic

Bernstein

Chebyshev

Content

Dickson

GaussLemma

HilbertPoly

Ideal

IntegralNormalization

IrreducibleRing

Nilpotent

Opposites

Pochhammer

Quotient

Radical

RationalRoot

ScaleRoots

Selmer

SeparableDegree

Tower

UniqueFactorization

Vieta

Wronskian

PowerSeries

Basic

Derivative

Inverse

Order

PiTopology

Trunc

WellKnown

Regular

IsSMulRegular

RegularSequence

RingHom

Finite

FinitePresentation

FiniteType

Flat

Injective

Integral

Locally

StandardSmooth

Surjective

RootsOfUnity

AlgebraicallyClosed

Basic

Complex

EnoughRootsOfUnity

Lemmas

Minpoly

PrimitiveRoots

SimpleRing

Basic

Defs

Field

Matrix

Smooth

Basic

Kaehler

Pi

StandardSmooth

TensorProduct

Basic

Finite

Free

MvPolynomial

Nontrivial

Pi

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

Pi

Valuation

AlgebraInstances

Basic

ExtendToLocalization

Integers

Integral

LocalSubring

Minpoly

PrimeMultiplicity

Quotient

RamificationGroup

RankOne

ValExtension

ValuationRing

ValuationSubring

WittVector

Basic

Compare

Defs

DiscreteValuationRing

Domain

Frobenius

FrobeniusFractionField

Identities

InitTail

IsPoly

Isocrystal

MulCoeff

MulP

StructurePolynomial

Teichmuller

Truncated

Verschiebung

WittPolynomial

AdjoinRoot

AlgebraTower

Artinian

Bezout

Binomial

ChainOfDivisors

ClassGroup

Complex

Discriminant

DualNumber

EisensteinCriterion

EssentialFiniteness

EuclideanDomain

Extension

Filtration

FiniteLength

FinitePresentation

FiniteStability

FiniteType

Fintype

FreeCommRing

FreeRing

Generators

Henselian

HopfAlgebra

Idempotents

IntegralDomain

Invariant

IsAdjoinRoot

IsPrimary

IsTensorProduct

Lasker

LaurentSeries

LinearDisjoint

LittleWedderburn

MatrixAlgebra

MaximalSpectrum

Multiplicity

Nakayama

NormTrace

Nullstellensatz

OrzechProperty

Perfection

PiTensorProduct

PolynomialAlgebra

PowerBasis

Presentation

Prime

PrimeSpectrum

PrincipalIdealDomain

PrincipalIdealDomainOfPrime

QuotSMulTop

Radical

ReesAlgebra

RingHomProperties

RingInvo

SimpleModule

Support

SurjectiveOnStalks

ZMod

SetTheory

Cardinal

Aleph

Arithmetic

Basic

Cofinality

Continuum

CountableCover

Divisibility

ENat

Finite

Finsupp

Free

SchroederBernstein

Subfield

ToNat

UnivLE

Game

Basic

Birthday

Domineering

Impartial

Nim

Ordinal

PGame

Short

State

Nimber

Basic

Field

Ordinal

Arithmetic

Basic

CantorNormalForm

Enum

Exponential

FixedPoint

FixedPointApproximants

NaturalOps

Notation

Principal

Rank

Topology

Surreal

Basic

Dyadic

Multiplication

ZFC

Basic

Ordinal

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

Elementwise

MonoidalComp

Reassoc

Slice

ToApp

Continuity (file)

Init

Explode (file)

Datatypes

Pretty

Finiteness (file)

Attr

FunProp (file)

Attr

ContDiff

Core

Decl

Differentiable

Elab

FunctionData

Mor

RefinedDiscrTree

StateList

Theorems

ToBatteries

Types

GCongr (file)

Core

CoreAttrs

ForwardAttr

Linarith (file)

Oracle

SimplexAlgorithm (file)

Datatypes

Gauss

PositiveVector

SimplexAlgorithm

FourierMotzkin

Datatypes

Frontend

Lemmas

Parsing

Preprocessing

Verification

LinearCombination (file)

Lemmas

Linter (file)

AdmitLinter

DocPrime

FlexibleLinter

GlobalAttributeIn

HashCommandLinter

HaveLetLinter

Header

Lint

MinImports

Multigoal

OldObtain

PPRoundtrip

RefineLinter

Style

TextBased

UnusedTactic

UpstreamableDecl

Measurability (file)

Init

Monotonicity (file)

Attr

Basic

Lemmas

Nontriviality (file)

Core

NormNum (file)

Basic

BigOperators

Core

DivMod

Eq

GCD

Ineq

Inv

IsCoprime

LegendreSymbol

NatFib

NatSqrt

OfScientific

Pow

PowMod

Prime

Result

Positivity (file)

Basic

Core

Finset

ReduceModChar (file)

Ext

Relation

Rfl

Symm

Ring (file)

Basic

Compare

PNat

RingNF

Sat

FromLRAT

Simps

Basic

NotationClass

ToAdditive (file)

Frontend

Widget

Calc

CommDiag

CongrM

Conv

GCongr

InteractiveUnfold

SelectInsertParamsClass

SelectPanelUtils

StringDiagram

Abel

AdaptationNote

Algebraize

ApplyAt

ApplyCongr

ApplyFun

ApplyWith

Basic

ByContra

Cases

CasesM

Change

Check

Choose

Clean

ClearExcept

ClearExclamation

Clear_

Coe

Common

ComputeDegree

CongrExclamation

CongrM

Constructor

ContinuousFunctionalCalculus

Contrapose

Conv

Convert

Core

DeclarationNames

DefEqTransformations

DeprecateTo

DeriveFintype

DeriveToExpr

DeriveTraversable

Eqns

Eval

ExistsI

ExtendDoc

ExtractGoal

ExtractLets

FBinop

FailIfNoProgress

FieldSimp

FinCases

Find

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

PPWithUniv

Peel

Polyrith

ProdAssoc

ProjectionNotation

Propose

ProxyType

PushNeg

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

TermCongr

ToExpr

ToLevel

Trace

TryThis

TypeCheck

TypeStar

UnsetOption

Use

Variable

WLOG

Zify

Testing

Plausible

Functions

Sampleable

Testable

Topology

Algebra

Algebra (file)

Rat

Category

ProfiniteGrp

Basic

Constructions (file)

DomMulAct

Group

Basic

Compact

OpenMapping

Quotient

SubmonoidClosure

TopologicalAbelianization

InfiniteSum

Basic

Constructions

Defs

ENNReal

Field

Group

GroupCompletion

Module

NatInt

Nonarchimedean

Order

Real

Ring

Module

Alternating

Basic

Topology

Multilinear

Basic

Bounded

Topology

Basic

Cardinality

CharacterSpace

Determinant

Equiv

FiniteDimension

LinearMap

LinearMapPiProd

LinearPMap

LocallyConvex

ModuleTopology

Simple

Star

StrongTopology

UniformConvergence

WeakBilin

WeakDual

Nonarchimedean

AdicTopology

Bases

Basic

Completion

TotallyDisconnected

Order

Archimedean

Field

Floor

Group

LiminfLimsup

UpperLower

ProperAction

Basic

ProperlyDiscontinuous

Ring

Basic

Ideal

SeparationQuotient

Basic

Section

UniformGroup

Basic

Defs

Valued

LocallyCompact

NormedValued

ValuationTopology

ValuedField

Affine

ClopenNhdofOne

ClosedSubgroup

ConstMulAction

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

Localization

Monoid

MulAction

MvPolynomial

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

PontryaginDual

ProperConstSMul

Semigroup

Star

StarSubalgebra

Support

UniformConvergence

UniformField

UniformFilterBasis

UniformMulAction

UniformRing

WithZeroTopology

Baire

BaireMeasurable

CompleteMetrizable

Lemmas

LocallyCompactRegular

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Category

CompHaus

Basic

EffectiveEpi

Limits

Projective

CompHausLike

Basic

EffectiveEpi

Limits

SigmaComparison

LightProfinite

AsLimit

Basic

EffectiveEpi

Extend

Limits

Sequence

Profinite

AsLimit

Basic

CofilteredLimit

EffectiveEpi

Extend

Limits

Nobeling

Product

Projective

Stonean

Adjunctions

Basic

EffectiveEpi

Limits

TopCat

Limits

Basic

Cofiltered

Konig

Products

Pullbacks

Adjunctions

Basic

EffectiveEpi

EpiMono

OpenNhds

Opens

Sphere

Yoneda

Born

CompactlyGenerated

Compactum

FinTopCat

Locale

Sequential

TopCommRingCat

UniformSpace

Compactification

OnePoint

OnePointEquiv

Compactness

Compact

CompactlyGeneratedSpace

DeltaGeneratedSpace

Exterior

Lindelof

LocallyCompact

Paracompact

PseudometrizableLindelof

SigmaCompact

Connected

Basic

Clopen

LocallyConnected

PathConnected

Separation

TotallyDisconnected

ContinuousMap

Bounded

Basic

Star

Algebra

Basic

BoundedCompactlySupported

CocompactMap

Compact

CompactlySupported

ContinuousMapZero

Defs

Ideals

Interval

Lattice

LocallyConstant

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

UniformSpace

Hom

ContinuousEval

ContinuousEvalConst

Open

Homotopy

Basic

Contractible

Equiv

HSpaces

HomotopyGroup

Path

Product

Instances

AddCircle

CantorSet

Complex

Discrete

ENNReal

ENat

EReal

Int

Irrational

Matrix

NNReal

Nat

PNat

Rat

RatLemmas

Real

RealVectorSpace

Sign

TrivSqZeroExt

ZMod

ZMultiples

LocallyConstant

Algebra

Basic

Maps

Proper

Basic

CompactlyGenerated

UniversallyClosed

Basic

OpenQuotient

MetricSpace

ProperSpace (file)

Lemmas

Pseudo

Basic

Constructions

Defs

Lemmas

Pi

Real

Ultra

Basic

ContinuousMaps

TotallySeparated

Algebra

Antilipschitz

Basic

Bilipschitz

Bounded

CantorScheme

CauSeqFilter

Cauchy

Closeds

Completion

Contracting

Defs

Dilation

DilationEquiv

Equicontinuity

Gluing

GromovHausdorff

GromovHausdorffRealized

HausdorffDimension

HausdorffDistance

Holder

HolderNorm

Infsep

IsometricSMul

Isometry

Kuratowski

Lipschitz

MetricSeparated

PartitionOfUnity

Perfect

PiNat

Polish

Sequences

ShrinkingLemma

ThickenedIndicator

Thickening

Metrizable

Basic

ContinuousMap

Uniformity

Urysohn

Order (file)

Category

AlexDisc

FrameAdjunction

Hom

Basic

Esakia

Basic

Bornology

Bounded

Compact

DenselyOrdered

ExtendFrom

ExtrClosure

Filter

IntermediateValue

IsLUB

Lattice

LawsonTopology

LeftRight

LeftRightLim

LeftRightNhds

LocalExtr

LowerUpperTopology

Monotone

MonotoneContinuity

MonotoneConvergence

NhdsSet

OrderClosed

OrderClosedExtr

PartialSups

Priestley

ProjIcc

Rolle

ScottTopology

T5

UpperLowerSetTopology

Separation

Basic

CompletelyRegular

CountableSeparatingOn

GDelta

Hausdorff

NotNormal

Profinite

Regular

SeparatedNhds

Sets

Closeds

Compacts

Opens

Order

Sheaves

SheafCondition

EqualizerProducts

OpensLeCover

PairwiseIntersections

Sites

UniqueGluing

CommRingCat

Forget

Functors

Init

Limits

LocalPredicate

LocallySurjective

MayerVietoris

PUnit

Presheaf

PresheafOfFunctions

Sheaf

SheafOfFunctions

Sheafify

Skyscraper

Stalks

Spectral

Hom

UniformSpace

AbsoluteValue

AbstractCompletion

Ascoli

Basic

Cauchy

Compact

CompactConvergence

CompareReals

CompleteSeparated

Completion

Dini

Equicontinuity

Equiv

HeineCantor

Matrix

OfCompactT2

OfFun

Pi

Separation

UniformConvergence

UniformConvergenceTopology

UniformEmbedding

VectorBundle

Basic

Constructions

Hom

AlexandrovDiscrete

ApproximateUnit

Bases

Basic

CWComplex

Clopen

ClopenBox

CompactOpen

Constructions

ContinuousOn

Covering

DenseEmbedding

DerivedSet

DiscreteQuotient

DiscreteSubset

ExtendFrom

Exterior

ExtremallyDisconnected

FiberPartition

Filter

Germ

Gluing

Homeomorph

IndicatorConstPointwise

Inseparable

Irreducible

IsLocalHomeomorph

JacobsonSpace

KrullDimension

List

LocalAtTarget

LocallyClosed

LocallyFinite

NhdsSet

NoetherianSpace

OmegaCompletePartialOrder

Partial

PartialHomeomorph

PartitionOfUnity

Perfect

PreorderRestrict

QuasiSeparated

RestrictGen

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

ParseCommand

Qq

SleepHeartbeats

Superscript

SynthesizeUsing

Tactic

TermBeta

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

Delab

Macro

Match

MetaM

SortLocalDecls

Typ

Std (file)

Data (file)

DHashMap (file)

Internal

AssocList

Basic

Lemmas

List

Associative

Defs

HashesTo

Defs

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

Lemmas

Raw

RawDef

RawLemmas

HashMap (file)

AdditionalOperations

Basic

Lemmas

Raw

RawLemmas

HashSet (file)

Basic

Lemmas

Raw

RawLemmas

Internal (file)

Parsec (file)

Basic

ByteArray

String

Rat

Sat (file)

AIG (file)

RefVecOperator (file)

Fold

Map

Zip

Basic

CNF

Cached

CachedGates

CachedGatesLemmas

CachedLemmas

If

LawfulOperator

LawfulVecOperator

Lemmas

RefVec

Relabel

RelabelNat

CNF (file)

Basic

Dimacs

Literal

Relabel

RelabelFin

Tactic (file)

BVDecide (file)

Bitblast (file)

BVExpr (file)

Circuit (file)

Impl (file)

Operations

Add

Append

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

RotateLeft

RotateRight

ShiftLeft

ShiftRight

SignExtend

Sub

Udiv

Ult

Umod

ZeroExtend

Carry

Const

Expr

Pred

Var

Lemmas (file)

Operations

Add

Append

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

RotateLeft

RotateRight

ShiftLeft

ShiftRight

SignExtend

Sub

Udiv

Ult

Umod

ZeroExtend

Basic

Carry

Const

Expr

Pred

Var

Basic

BoolExpr (file)

Basic

Circuit

LRAT (file)

Internal

Formula (file)

Class

Implementation

Instance

Lemmas

RatAddResult

RatAddSound

RupAddResult

RupAddSound

Actions

Assignment

CNF

Clause

Convert

Entails

LRATChecker

LRATCheckerSound

PosFin

Actions

Checker

Parser

Normalize (file)

BitVec

Bool

Canonicalize

Equal

Prop

Reflect

Syntax

Time (file)

Date (file)

Unit

Basic

Day

Month

Week

Weekday

Year

Basic

PlainDate

ValidDate

DateTime (file)

PlainDateTime

Timestamp

Format (file)

Basic

Internal (file)

Bounded

UnitVal

Notation (file)

Spec

Time (file)

Unit

Basic

Hour

Millisecond

Minute

Nanosecond

Second

Basic

HourMarker

PlainTime

Zoned (file)

Database (file)

Basic

TZdb

TzIf

Windows

DateTime

Offset

TimeZone

ZoneRules

ZonedDateTime

Duration

docs (file)

Conv

Guide

Introduction

references (file)

Color scheme

darksystemlight