General documentation

index

foundational types

tactics

Library

Aesop (file)

Builder

Apply

Basic

Cases

Constructors

Default

Forward

NormSimp

Tactic

Unfold

BuiltinRules (file)

ApplyHyps

Assumption

DestructProducts

Ext

Intros

Rfl

Split

Subst

Forward

Match (file)

Types

State (file)

ApplyGoalDiff

Initial

UpdateGoal

LevelIndex

PremiseIndex

RuleInfo

SlotIndex

Substitution

Frontend (file)

Extension (file)

Init

Attribute

Basic

Command

RuleExpr

Saturate

Tactic

Index (file)

Basic

DiscrTreeConfig

Forward

RulePattern

Options

Internal

Public

Rule (file)

Basic

Forward

Name

RulePattern (file)

Cache

RuleSet (file)

Filter

Member

Name

RuleTac (file)

Forward (file)

Basic

Apply

Basic

Cases

Descr

ElabRuleTerm

GoalDiff

Preprocess

RuleTerm

Tactic

Script

Check

CtorNames

GoalWithMVars

Main

OptimizeSyntax

SScript

ScriptM

SpecificTactics

Step

StructureDynamic

StructureStatic

Tactic

TacticState

UScript

UScriptToSScript

Util

Search

Expansion (file)

Basic

Norm

Simp

Queue (file)

Class

ExpandSafePrefix

Main

RuleSelection

SearchM

Stats

Basic

Extension

File

Report

Tree

Data (file)

ForwardRuleMatches

AddRapp

Check

ExtractProof

ExtractScript

Free

RunMetaM

State

Stats

Tracing

Traversal

TreeM

UnsafeQueue

Util

Tactic (file)

Ext

Unfold

Basic

EqualUpToIds

OrderedHashSet

Unfold

UnionFind

UnorderedArraySet

BaseM

Check

Constants

EMap

ElabM

Exception

Main

Nanos

Percent

Saturate

Tracing

Batteries

Classes

Order

RatCast

CodeAction (file)

Attr

Basic

Deprecated

Match

Misc

Control

ForInStep

Basic

Lemmas

Nondet

Basic

AlternativeMonad

LawfulMonadState

Lemmas

OptionT

Data

Array

Basic

Match

Merge

BinomialHeap

Basic

Fin

Basic

Lemmas

List

Basic

Count

Lemmas

Pairwise

Perm

MLList

Basic

Nat

Basic

Lemmas

String

Basic

Matcher

UInt

Lean

Meta

Basic

DiscrTree

Expr

Inaccessible

InstantiateMVars

SavedState

UnusedNames

AttributeExtra

Except

Expr

HashMap

HashSet

MonadBacktrack

NameMapAttribute

PersistentHashMap

PersistentHashSet

Position

Syntax

TagAttribute

Linter (file)

UnnecessarySeqFocus

UnreachableTactic

Tactic

Lint (file)

Basic

Frontend

Misc

Simp

TypeClass

Alias

Basic

Case

Congr

Exact

GeneralizeProofs

HelpCmd

Init

OpenPrivate

PermuteGoals

SeqFocus

Trans

Unreachable

Util

Cache

ExtendedBinder

LibraryNote

ProofWanted

Logic

DerivedAlgGeo (file)

Algebra (file)

Category (file)

FGModuleCat (file)

Noetherian

Projective

Grp (file)

ForgetCorepresentable

Preadditive

Products

ModuleCat (file)

LinearDual (file)

Basic

Exact

Presheaf (file)

AB

ExteriorPower

Monoidal

Sections

Sheaf (file)

Presentation (file)

Extensions

Finite

Isomorphism

Locality

Over

Transport

Zero

AB

Cohomology

Exactness

GeneratingSections

Generator

Invertible

LocallyFree

Over

Tensor

Limits

Localization

Noetherian

ProjectiveResolution

Exact (file)

Sequence

Finsupp (file)

LaurentExponent

Homology (file)

DGCategory (file)

FullSubcategory (file)

Pretriangulated

Model (file)

Complexes

Linear

LinearCopower

Shift

Pretriangulated (file)

H0 (file)

AdjunctionComparison

AdjunctionCone

AdjunctionConePresentation

AdjunctionCotwistPresentation

Basic

ConeFunctor

Functor

FunctorTransport

HomCohomology

LinearObjectTwist

LinearObjectTwistAdjunction

NaturalTransformationCone

NaturalTransformationConeShift

ObjectTwist

Shift

ShiftedFunctor

Triangle

AdjunctionComparison

AdjunctionCone

Basic

Cone

ConeCategory

ConeExactness

Functor

FunctorCategory

FunctorCategoryShift

HomogeneousLift

HomogeneousShift

Lift

LinearObjectTwist

LinearObjectTwistAdjunction

LinearShiftHomology

LinearShiftIso

NaturalTransformationCone

NaturalTransformationShift

ObjectTwist

Rotate

ShiftIso

Adjunction

AdjunctionH0

AdjunctionH0Presentation

Basic

Copower

Functor

FunctorCategoryH0

H0

HorizontalComposition

Instances

Linear

LinearCopower

LinearCopowerAdjunction

LinearCopowerFunctor

LinearCopowerUnit

LinearEvaluation

LinearH0

LinearH0Homology

LinearHomFunctor

NaturalTransformation

NaturalTransformationH0

Opposite

Product

QuasiEquivalence

Shift

Whiskering

DerivedCategory (file)

BoundedAboveProjective (file)

Unitality

CohomologyObjectProperty (file)

Bounded

HomVanishing

Termwise

ExactFunctor (file)

Bounded

Coproducts

Ext (file)

AcyclicComparison

AcyclicGenerators

Adjunction

DimensionShift

FiniteGenerators

InjectiveResolutionNaturality

GrothendieckGroup (file)

Comparison

BoundedHeart

Coproducts

FGModuleCatInclusion

Heart

HeartHomology

HomComplexCohomology

HomComplexCohomologyBoundedComplexLocalization

HomComplexCohomologyDegreeZeroLocalization

HomComplexCohomologyFiniteReplacementLocalization

HomComplexCohomologyFiniteResolutionLocalization

HomComplexCohomologyIntLocalization

HomComplexCohomologyLinear

HomComplexCohomologyLocalization

HomComplexCohomologyLocalizationNaturality

HomFinite

Homology

KFlatResolution

KProjective

LinearDual

ModuleCatLocalization

ModuleCatLocalizationQh

Opposite

RightDerivedFunctorPlus

SingleTriangle

Embedding (file)

CochainComplex

Extend

StupidTruncGE

Homotopy (file)

FiniteCohomologyPresentation

FiniteCohomologyPresentationOfSupport

HomologyModel

ModuleCatFormality

Sigma

HomotopyCategory (file)

DGEnhancement (file)

Agreement

CommShift

DerivedSeam

Enhancement

FiniteCohomologyCopower

FiniteCohomologyCopowerK0

HomComplexFiniteCohomologyPresentation

KInjective

KProjective

LinearCopower

LinearCopowerFiniteFree

LinearEvaluationK0

LinearObjectTwistK0

Pretriangulated

Seam

ShiftComparison

Bounded

Coproducts

HomComplexCohomologyClassLocalization

HomComplexCohomologyHomotopy

HomComplexCohomologyHomotopyNaturality

HomComplexCohomologyIntLocalization

HomComplexCohomologyLinear

HomComplexCohomologyLocalization

HomComplexCohomologyNaturality

HomComplexLocalization

HomComplexPostcomp

HomComplexSingle

LeftResolution (file)

Augmented

HomologyZero

ShortComplex (file)

Limits

SpectralSequence (file)

ExtendHomologyNaturality

FilteredComplexSpectralObject

FilteredTotalComplex

FilteredTotalComplexAdjacent

FilteredTotalComplexAdjacentCore

FilteredTotalComplexFirstPageDifferential

FiniteStripTotal

SingleZeroTotal

TotalFlipNaturality

TotalQuasiIso

Bifunctor

CochainComplexFiniteProjectiveResolution

EulerCharacteristic

HomologicalBicomplex

HomologicalComplexFiniteDescent

HomologicalComplexLeftExact

HomologicalComplexLimits

HomologySequenceLemmas

Localization

Subcomplex

TotalComplex

Module (file)

GradedModule (file)

Localization

PowersCongr

Shift

TwistLocalization

Localization (file)

Cohomology

FiniteDescent

FixedTargetArrow

FixedTerminalThreeTerm

Kernels

LocalizedModule (file)

NestedSubmodule

NestedSubmoduleLeft

Submodule

TwoChartSubmodule

LocalizedRadical

MvPolynomial (file)

Cech (file)

Basic

Finite

Homotopy

Primitive

DivMonomial

Grading

LaurentBasis

LaurentBlock

LaurentFinite

LaurentHomotopy

LaurentProjection

NumericalPolynomial (file)

Basic

Order

NormalizedShift (file)

Basic

UniformContinuity

RelativeNumerical (file)

Basic

Overlattice

SaturatedQuotient

AlgebraicGeometry (file)

Cohomology (file)

Cech (file)

Affine

AffineBasisComparison

NegativeTwist

ProjectiveSpace

TopDegree

Vanishing

Derived (file)

AffineHomVanishing

AffineHypercohomology

AffineRGammaPlus

AffineRGammaPlusEvaluation

AffineVanishing

H0Sections

LineBundleExtLinear

UnitExt

UnitExtLinear

EulerCharacteristic (file)

Additivity

Basic

Finiteness (file)

Boundedness

CoherentExtGenerators

Devissage

FiniteDimensional

GlobalSections

Hom

LineBundleExt

LinearCech

LinearConnecting

Projective

ProjectiveSpace

ProjectiveSpaceCechHomology

ProjectiveSpaceCechScalars

ProjectiveSpaceScalars

ProjectiveSpaceTopFinite

ProjectiveVariety

RestrictedTwistExt

RestrictedTwistPresentation

ClosedImmersion

DerivedCategory (file)

Dqc (file)

Affine

AffineCoproducts

AffineDerivedEquivalence

AffineFamilyPseudofunctor

AffineGeometricCorePseudofunctor

AffineGeometricPseudofunctor

AffineIdentification

AffineKProjectiveCoherence

AffineKProjectiveDerivedPseudofunctor

AffineKProjectivePseudofunctor

AffineKProjectivePullback

AffineKProjectiveUnitality

AffineLocalizationPullback

AffineNonflatDerivedObject

AffineNonflatExample

AffinePullback

AffinePushforward

AffineQuasicoherentIdentification

AffineRealization

BoundedCoherent

Comparison

Identification

KFlatTensor

Linear

TermwiseQuasicoherent

Families (file)

AffineCoherentLocalizationComparison

AffineKFlatPullback

AffineLocalizationKFlatComparison

BaseChangeAdjunction

BaseChangeBoundedAmplitude

BaseChangeCategory

BaseChangeData

BaseChangeDecomposition

BaseChangeFaithfulness

BaseChangeFiberCoefficient

BaseChangeGeneration

BaseChangeHomReduction

BaseChangeKFlatSLinearity

BaseChangeLinearity

BaseChangePerfectEnvelopeOrthogonal

BaseChangeProjection

BaseChangeProjectionArrowExtension

BaseChangeProposition315

BaseChangePushforward

BaseChangeSLinearity

BaseChangeSequence

BaseChangeSequenceFunctoriality

BaseChangeShiftedGeneratorOrthogonal

BaseChangeSourceSequence

BaseChangeTStructureRestriction

BaseChangeTensorDuality

BaseChangeTensorProjectionFormula

BoundedGeometry

CoherentPullback

CoherentPullbackCoherence

CoherentPushforward

CoherentPushforwardCoherence

DerivedPullbackCoherence

DerivedPullbackLaws

DerivedPullbackShift

DerivedPushforward

ExactPullback

ExactPullbackCoherence

ExactPullbackDqc

FiniteType

FlatPullback

FlatPullbackResolution

KFlatBaseChange

KFlatBaseChangeFunctors

KFlatPullback

KFlatQuasicoherentPullback

KProjectivePullback

LeftDerivedPullback

OpenImmersionPullback

OpensBaseChange

PerfectPullback

PullbackAcyclicResolution

RelativeLocalizationLinearity

RelativeLocalizationScalars

ResidueFiber

RightDerivedPushforward

SLocal

Scheme

SchemeDerived

Theorem53

FourierMukai (file)

KernelAdjunction

KernelAssociativity

KernelComposition

KernelConvolution

KernelCorrespondence

KernelDualizingTwist

KernelSwap

KernelUnit

KernelUnitConvolution

Perfect (file)

Relative

Stability (file)

BoundedCoherentBaseChange

BoundedCoherentPullback

BoundedCoherentPushforward

DerivedPullback

FourierMukaiAction

K3MukaiTilt

K3MukaiTiltScheme

MassHom

MassHomTheorem75

SLocal

Tensor (file)

BoundedAboveKFlat

BoundedCoherent

BoundedMonoidal

Coherent

FiniteKFlat

FreeYonedaKFlat

LeftDerivedTensor

Relative

Unbounded

Basic

CartierDivisor

Coherent

DivisorSequence

TwistedPushforward

Divisors (file)

AssociatedSheaf (file)

Construction

PicardMap

RationalSections

Cartier

CartierLineBundle

Determinant

Dual

Effective

EffectiveLineBundle

FiniteLocallyFreePullback

LineBundleDual

PicardGroup

Symmetric

Duality (file)

Canonical (file)

Basic

Derived

Descent

Differentials

Serre (file)

Bilinear

Categorical

Cohomology

IntersectionTheory (file)

ChernCharacter (file)

Basic

Surface

Surface (file)

Number

Snapper

Modules (file)

Affine (file)

BasicOpen

Comparison

Epi

Equivalence

Extension

Finiteness

Gluing

Coherent (file)

Abelian (file)

Basic

Extensions

Kernels

Affine (file)

BasicOpen

BasicOpenArrow

BasicOpenLocalizedSubobject

BasicOpenRestriction

BasicOpenSubobject

BasicOpenSubobjectClassification

Comparison

Free

Localization

LocalizedSubobject

Basic (file)

Definitions

Isomorphism

Descent (file)

Locality

Pushforward (file)

Affine

Finite

Iso

AffineChart

Linear

Noetherian

Pullback

StructureSheaf

SubobjectLocality

ExteriorPower (file)

Restriction

Pullback (file)

AffineLocalizationUnit

AffineSpec

FixedBaseOpenSections

FixedBaseSections

Invertible

KFlatQuasiIso

LocallyFree

Monoidal

Presentation

Restriction

ScalarExtendedOpenSections

ScalarExtendedSections

ScalarExtendedTwoOpen

SliceSiteBaseChange

Stalk

StalkQuasiIso

Pushforward (file)

Action

Affine

BaseChange

ClosedImmersion

Iso

Quasicoherent (file)

Coproducts

Extensions

Kernels

Pullback

Restriction (file)

OpenImmersion

Sections

StructureSheaf

Tensor (file)

Basic

Colimits

Complex

ComplexColimits

Flat

Invertible

LineBundle

LineBundleLinear

Linear

Monoidal

Picard

Stalk

AB

FixedBaseSheaf

FixedBaseSheafLocalization

Flasque

Flat

FlatGenerators

FlatResolutionTotalization

LocalCombination

LocallySurjective

Tilde

Moduli (file)

HarderNarasimhan (file)

DedekindProblem

RelativeFiltration

PerfectComplex (file)

AffineFamilyRelativePerfect

AffineFamilyRelativePerfectPseudofunctor

Algebraicity

BigZariski

Boundedness

Comparison

Presheaf

Pullback

Quot (file)

Basic

ParameterSpace

Semistability (file)

FiniteType

Locus

LocusProbes

SchemeProbes

Morphisms (file)

AlmostDisconnected

FiltrationProperty

Numerical (file)

Core (file)

CharacteristicClasses

Definitions

GradedBasis

Examples (file)

Fourfold (file)

CalabiYauWalls

ProjectiveSpaceWalls

Surface (file)

BlowUpPlane

BlowUpPlaneSlice

BlowUpPlaneWalls

K3MukaiComparison

ProjectivePlaneCharge

RankOneRealization

RankOneWalls

SmoothQuadric

SmoothQuadricCharge

Threefold (file)

CalabiYauWalls

ProjectiveSpaceWalls

GrothendieckGroup (file)

CategoricalChargeK3

CentralChargeK3

Discriminant

Dual

EulerPairing

EulerTransfer

Lattice

MukaiVector

RadicalKernel

Realization

Models (file)

DimensionZero (file)

Point

Fourfold (file)

CalabiYau

LinearSection

ProjectiveSpace

Surface (file)

Abelian

Comparison

Enriques

K3

K3Mukai

K3MukaiIntegral

ProjectivePlane

RankOne

Threefold (file)

CalabiYau

LinearSection

ProjectiveSpace

MonogenicRing

Mukai (file)

Integral

Pairing

SqrtTodd

SqrtToddK3

VectorClass

VectorClassK3

RiemannRoch (file)

Enriques

General

K3

Specializations (file)

Fourfold

Surface

Threefold

Stability (file)

BMT

BogomolovGieseker

DivisorialChargeNumerical

DivisorialChargeScalarExtension

DivisorialDiscriminant

DivisorialMukai

DivisorialSupport

DivisorialWallCircle

DivisorialWallTransport

ExponentialTwist

PolarisedMukaiTransport

PolarisedWallTransport

PolarisedWallTransportComparison

Slope

SlopeK3

SurfaceChargeNumerical

ThreefoldTiltTransport

ThreefoldWallTransport

TwistedChern

WallTransport

ProjectiveSpectrum (file)

Modules (file)

AssociatedSheaf

AwayChart

ChartExtension

ChartGeneration

ChartProj

ChartScalar

ChartUnitTwist

Finiteness

Frac

FracSection

GlobalGeneration

Glue

GlueUniform

ProjectiveSpace

StructureModule

TensorTwist

TwistAdd

TwistApp

TwistBridge

TwistChart

TwistCoherence

TwistComparison

TwistGenerated

TwistInverse

TwistInvertible

TwistMultiplication

TwistSection

TwistingSheaf

BasicOpenLemmas

Integral

ProjectiveSpaceProperties

ProjectiveSpaceVariety

StructureSections

RiemannRoch (file)

HigherDimension (file)

Hirzebruch

Surface (file)

Assembly

Devissage

Divisor

NumericalVariety

ToddData

Reconstruction

Sites (file)

Comparison

QuasiCompact

Stability (file)

Gieseker (file)

Basic

Slope (file)

HarderNarasimhan (file)

Consequences

Existence

HeartTransport

MaximalDestabilizing

Seesaw

SlopeBoundedness

Splice

StrictDrop

Basic

Coefficients

Comparison

HilbertPolynomial

Purity

Stacks (file)

Algebraic

AlgebraicStack

Descent

Representable

Surface (file)

Enriques (file)

Basic

Collection

Exceptional

PaperBlocks

PaperExtension

PaperMatching

PaperObjects

PaperTorelli

Residual

K3

Spherical

SphericalCategorical

SphericalMukai

Variety (file)

Basic

Numerical

Projective

CohomologyPushforward

AlgebraicTopology (file)

ExtraCodegeneracy

Analysis (file)

Complex (file)

HalfPlane

PhaseFiniteSums

PhaseGeometry

Convex (file)

ComplexPolygonalPath (file)

Basic

Perimeter

CategoryTheory (file)

Abelian (file)

SerreClass (file)

FullSubcategory

Weak

Stability (file)

Uniqueness (file)

Destabilizing

Extrema

MonoDescent

SubobjectLattice

Tail

Weak (file)

Cutoff

CutoffSlope

Extrema

HNTransport

HarderNarasimhan

Slope

SlopeCutoff

SlopeGeometry

SlopeOrder

SlopeTop

SlopeTransport

Splitting

Tail

Truncation

Basic

Charge

Cutoff

HNPolygon

HarderNarasimhan

PhaseGeometry

PhaseMonotone

SimpleCharge

Slope

SlopeCutoff

SlopeThreshold

Splitting

Subobject

Truncation

QuasiAbelian

Bicategory (file)

Adjunction (file)

Basic

Cat

Functor (file)

Cat (file)

ObjectProperty (file)

UniversallyStable

Transport

LocallyDiscrete

Basic

GrothendieckGroup (file)

Abelian

ExactSequence

Functorial

Presentation

Limits (file)

Preserves (file)

Shapes (file)

Products

Composition

Naturality

Reflective

Shapes (file)

FiniteProducts

ZeroMorphisms

Linear (file)

SerreFunctor (file)

Basic

Conjugation

Equivalence

Uniqueness

Adjunction

Opposite

Yoneda

Localization (file)

Coproducts

SmallShiftedHom

Moduli (file)

Boundedness

Monoidal (file)

Triangulated

MorphismProperty (file)

Limits

ObjectProperty (file)

Bifunctor

Lift

Orthogonal

Preadditive (file)

CompactObject

Shift (file)

CommShift

FunctorCategory

Sites (file)

Descent (file)

StackInGroupoids (file)

Discrete

Morphism

Representable

SheafCohomology (file)

Cech (file)

Bicomplex

Comparison

ComplexNaturality

Contractible

Differential

InitialPage

ModuleForget

SmallSiteResolution

TotalComparison

Sheaves (file)

CohomologyPushforward

CohomologyShortExact

ConstantPullback

CoversTop

CoversTop

Over

Subobject (file)

JointReflection

LocalizedHomArrowExtension

NoetherianObject

Triangulated (file)

CompactlyGenerated (file)

Brown

Coaisle

Existence

FiniteSupport

IndExtension

IndFilteredColimits

Polishchuk

Projection

Telescope

Thick

DGEnhancement (file)

H0 (file)

ConeFunctor

HomCohomologyEuler

LinearEvaluationK0

LinearObjectTwistK0

MorphismCone

NaturalTransformationConeK0

ObjectTwistK0

Basic

Exact

GrothendieckGroup

Dimension (file)

Composition

ExtensionClosureComparison

Functor

GenerationTime

Rouquier

Families (file)

BaseChange

FourierMukai (file)

AdjointAssembly

Adjunction

AdjunctionUnitKernel

Autoequivalence

Basic

Convolution

CounitKernel

DGAdjunctionCotwistComparison

DGAdjunctionDualCotwistComparison

DGAdjunctionDualTwistComparison

DGAdjunctionPresentation

DGAdjunctionTwistComparison

DGAdjunctionTwistCotwistAutoequivalence

DualCotwistKernel

DualTwistKernel

ExceptionalExtension

ExceptionalInduction

GrothendieckGroup

KernelCone

KernelConeNormalization

KernelTransformation

Witness

Generators (file)

Composition

Functor

GrothendieckGroup (file)

Basic

Biproduct

EulerForm

Functorial

HeartComparison

HomFiniteWitness

RankOne

Realization

Opposite (file)

Linear

SemiorthogonalDecomposition (file)

AdjacentExt

Admissible

Amplitude

Basic

Blocks

Collection

CompactClosure

DerivedField

Examples

Exceptional

Mutation

Orientation

Projection

ProjectionArrowExtension

ProjectionFunctorMate

Restriction

Strong

SerreFunctor (file)

Classification

Enriques

Euler

Exactness

Matching

Objects

ProjectionObjects

Shift

Transport

SphericalTwist (file)

Autoequivalence

Basic

Braid

BraidStatement

Definition

EnhancedAdjunctionComparison

EnhancedFunctor

EnhancedFunctorH0

EnhancedFunctorK0

GrothendieckGroup

LinearObjectTwistK0

Mukai

ObjectTwistData

ObjectTwistK0

StabilityAction

StabilityCondition (file)

CentralCharge (file)

Divisorial (file)

Charge

Coordinates

Discriminant

Mukai

Slice

Todd

Exponential (file)

Comparison

Divisorial

Kernel

Twist

Mukai (file)

Charge

Chart

Orientation

Positivity

Numerical (file)

Surface

SurfaceFamily

Threefold

Family

Quadratic

Chambers (file)

Action

Basic

Topology

Families (file)

CategoricalOrdinary

FiberwiseOrdinary

FiberwiseSupport

Ordinary

PreStabilityBaseChange

StabilityOverField

Foundation (file)

Deformation (file)

BoundaryTransport

ChargePerturbation

ConnectedComponent

DeformedCuts

DeformedHom

DeformedPhaseControl

DeformedPredicate

DeformedShift

DeformedSlicing

DeformedTriangulated

DeformedTruncation

FiniteLengthHN

FirstStrictSES

GlobalHN

GlobalTruncation

HNExistence

HeartImage

IntervalIndependence

LocalComparison

LocalFiniteness

LocalHomeomorphism

LocalInjectivity

LocalSurjectivity

MidpointHeart

NearIdentity

PhaseArithmetic

PhaseConfinement

PhaseSum

PhiPlusHN

PhiPlusMDQ

PhiPlusReduction

PhiPlusSplit

PullbackCokernel

RelativePhase

SeminormComparison

SkewedStability

SlicingDistance

StabilitySeminorm

StabilityTopology

StrictMDQ

TargetTransport

Theorem

Slicing (file)

IntervalComparisons

IntervalFiniteTransfer

IntervalPreabelian

IntervalStrictness

PreStabilityCondition

StabilityCondition

Mass (file)

Subadditivity (file)

Triangle (file)

Consequences

HeartObservable

HeartShortExact

MassAdditivity

MassTransport

PhaseOne

CohomologyExactness

HNPolygonComparison

Basic

Uniqueness

MassHom (file)

Algebraic

AlgebraicWitness

Basic

FieldExtension

FiniteDistance

FullSupport

Generator

JordanHolder

Stable

Transfer

Metric (file)

Distance (file)

Basic

Separation

Topology

Isometry (file)

Full

Phase

Hausdorff

Mukai (file)

Ambient

Assembly

Charge

GeometricInput

NumericalCases

Slope

Tilting

Phase (file)

Order (file)

Basic

Bayer

Characterizations

Cofiltration

Equivariance

Functoriality

Transfer (file)

Adjoint

BaseChange

Basic

Bayer

Equivariance

HN

IndExtensions

InducedTStructures

Inducing

LocallyFinite

Metric

Phase

PreStability

Support (file)

Divisorial

Semistable

Transfer

Symmetry (file)

Autoequivalence (file)

Foundations (file)

FiniteLength

Slicing (file)

Quotient

Strict

Transport

Stability (file)

ClassMap

Composition

Transport

FourierMukai

SerreFunctor

Combined (file)

Action

Components

Effective

LatticeAut

OrbitSpace

PeriodMap

ProperDiscontinuity

Topology

GLTilde (file)

Action (file)

Continuous

JointContinuous

PreStability

Slicing

Stability

Walls (file)

Divisorial (file)

Circle

Region

Signature

Slice

Numerical (file)

Basic

ChargeFamily

Discriminant

Nested

Spherical (file)

Basic

DivisorialRegion

Finiteness

WallComparison

Threefold (file)

Basic

Tilt

TiltComparison

Alignment

Rotation

Weak (file)

Basic (file)

ChargeRay

Definitions

Families (file)

Basic

Weak

Foundation (file)

Slicing (file)

BoundaryFactors

BoundaryTruncation

CoreConsequences

CutoffTruncation

FiltrationOperations

HeadTail

IntervalHeart

IntrinsicPhaseBounds

IntrinsicPhases

PhaseBounds

PhaseCutClosure

PhaseShift

PhaseTruncation

TwoHeartEmbedding

HeartDatum

IntervalCategory

HarderNarasimhan (file)

Ambient

Heart

Heart (file)

Equivalence

EquivalenceReverse

HomVanishing

Noetherian

Mass (file)

Basic

Uniqueness

Support (file)

Predicate (file)

Basic

IntegralRealQuotient

Quadratic

Quotient

Uniform

ZeroChargeLattice

Basic

Quadratic

Tilting (file)

Cohomology (file)

Basic

Exactness

Homological

Sequence

Shift

Semistable (file)

Classification

SemistableTransfer

TiltGeometry

TiltedHeart

ZeroCharge

Source (file)

Charge

Support

Theorems

TorsionPair (file)

Basic

CutoffPhase

Heart

HeartAdapter

HnTiltHeart

HnTiltStabilityFunction

Slope

SourceSlope

StabilityFunction

WeakHnTilt

WeakStabilityFunction

Assembly

HarderNarasimhan

Noetherian

PreStability

Property

TStructure (file)

Aisle

AisleProjection

Exactness

HeartBridge

HomComparison

ImageFactorisation

Local

Restriction

Retracts

Shift

ShiftNaturality

TruncationFiniteness

CompactObject

ExactFunctorFamily

ExtensionClosure

FullSubcategory

FunctorIsoShiftCompatibility

LinearCoyoneda

LinearYoneda

PostnikovTower

PretriangulatedAxioms

ShiftFunctor

TriangleFunctorNormalization

FiniteFiltration

SubobjectCorrespondence

SubobjectEquivalence

LinearAlgebra (file)

BilinearForm (file)

Lorentzian (file)

Diagonal

TimeCone

HodgeIndex

Hyperbolic

RankTwo

Reflection

Complex

Coordinates

ExteriorPower (file)

Semilinear

Top

FiniteDimensional (file)

Lemmas

Lattice (file)

Arithmetic (file)

TorsionFree

Mukai (file)

Basic

RankTwo

RealForm

RealFormSignature

Reflection

Numerical (file)

RankTwo

IsotropicSequence

Matrix

GeneralLinearGroup

UniversalCover (file)

Basic

ComplexRepresentation

Fibre

Map

SourceTopology

Surjectivity

TopologicalGroup

Positive

PolarDecomposition

QuadraticForm (file)

Bounds

ComplexPairing

ComplexPairingSignature

Continuous

OrthogonalityCutNonempty

OrthogonalityFiniteness

OrthogonalityLocus

OrthogonalityRegion

PositiveFrame

PositiveFrameOpen

PositiveFrameOrientation

PositivePlane

SignatureAdditive

GradedBasis

RingTheory (file)

GradedAlgebra (file)

HomogeneousLocalization (file)

Domain

Spectrum (file)

Prime (file)

BasicOpen

CoversTop

Topology (file)

Category (file)

TopCat (file)

Opens (file)

CoversTop

Final

Limits

Covering

Basic

Sheaves (file)

Cech (file)

BasisComparison

Boundedness

FreeAbelianYonedaStalk

GlobalComparison

InjectiveAcyclic

InjectiveFlasque

ModuleTensor (file)

StalkTensor

Basis

CohomologyPushforward

Flasque

ModuleStalk

ModuleStalkSheafification

ModulesCohomology

PushforwardStalks

StalkW

IrreducibleCover

ImportGraph

Graph

TransitiveClosure

Imports

ImportGraph

Redundant

RequiredModules

Lean

Environment

Tools (file)

FindHome

ImportDiff

MinImports

RedundantImports

Init (file)

Control (file)

Lawful (file)

MonadAttach (file)

Instances

Lemmas

MonadLift (file)

Basic

Instances

Lemmas

Basic

Instances

Lemmas

Basic

Do

EState

Except

ExceptCps

Id

MonadAttach

Option

Reader

State

StateCps

StateRef

Data (file)

Array (file)

Lex (file)

Basic

Lemmas

QSort (file)

Basic

Sort (file)

Basic

Lemmas

Subarray (file)

Split

Attach

Basic

BasicAux

BinSearch

Bootstrap

Count

DecidableEq

Erase

Extract

FinRange

Find

GetLit

InsertIdx

InsertionSort

Int

Lemmas

MapIdx

Mem

MinMax

Monadic

Nat

OfFn

Perm

Range

Set

TakeDrop

Zip

BitVec (file)

Basic

BasicAux

Bitblast

Bootstrap

Decidable

Folds

Lemmas

ByteArray (file)

Basic

Bootstrap

Extra

Lemmas

Char (file)

Basic

Lemmas

Order

Ordinal

Dyadic (file)

Basic

Instances

Inv

Round

Fin (file)

Basic

Bitwise

Fold

Iterate

Lemmas

Log2

OverflowAware

FloatArray (file)

Basic

Format (file)

Basic

Instances

Macro

Syntax

Int (file)

Bitwise (file)

Basic

Lemmas

DivMod (file)

Basic

Bootstrap

Lemmas

Pow

Basic

Compare

Cooper

Gcd

Lemmas

LemmasAux

Linear

OfNat

Order

Pow

Repr

ToString

Iterators (file)

Combinators (file)

Monadic (file)

Append

Attach

FilterMap

FlatMap

Take

ULift

Append

Attach

FilterMap

FlatMap

Take

ULift

Consumers (file)

Monadic (file)

Access

Collect

Loop

Partial

Total

Access

Collect

Loop

Partial

Stream

Total

Internal (file)

LawfulMonadLiftFunction

Lemmas (file)

Combinators (file)

Monadic (file)

Append

Attach

FilterMap

FlatMap

Take

ULift

Append

Attach

FilterMap

FlatMap

Take

ULift

Consumers (file)

Monadic (file)

Collect

Loop

Access

Collect

Loop

Monadic

Basic

Producers (file)

Monadic (file)

List

List

Basic

Producers (file)

Monadic (file)

List

List

Basic

PostconditionMonad

ToIterator

List (file)

Int (file)

Prod

Sum

Nat (file)

BEq

Basic

Count

Erase

Find

InsertIdx

Modify

Pairwise

Perm

Prod

Range

Sublist

Sum

TakeDrop

Scan (file)

Basic

Lemmas

Sort (file)

Basic

Impl

Lemmas

SplitOn (file)

Basic

Lemmas

Attach

Basic

BasicAux

Control

ControlImpl

Count

Erase

FinRange

Find

Impl

Lemmas

Lex

MapIdx

MinMax

MinMaxIdx

MinMaxOn

Monadic

Notation

OfFn

Pairwise

Perm

Range

Sublist

TakeDrop

ToArray

ToArrayImpl

Zip

Nat (file)

Bitwise (file)

Basic

Lemmas

Div (file)

Basic

Lemmas

Power2 (file)

Basic

Lemmas

Sqrt (file)

Basic

Lemmas

Basic

Compare

Control

Coprime

Dvd

Fold

Gcd

Lcm

Lemmas

Linear

Log2

MinMax

Mod

Order

SOM

Simproc

ToString

Option (file)

Array

Attach

Basic

BasicAux

Coe

Function

Instances

Lemmas

List

Monadic

Ord (file)

Array

Basic

BitVec

SInt

String

UInt

Vector

Order (file)

Classes

ClassesExtra

Factories

FactoriesExtra

Lemmas

LemmasExtra

MinMaxOn

Opposite

Ord

PackageFactories

Range (file)

Polymorphic (file)

Internal

SignedBitVec

Basic

BitVec

Char

Fin

GetElemTactic

Instances

Int

IntLemmas

Iterators

Lemmas

Map

Nat

NatLemmas

PRange

RangeIterator

SInt

Stream

UInt

UpwardEnumerable

Basic

Lemmas

Rat (file)

Basic

Lemmas

SInt (file)

Basic

Bitwise

Float

Float32

Lemmas

Slice (file)

Array (file)

Basic

Iterator

Lemmas

List (file)

Basic

Iterator

Lemmas

Basic

InternalLemmas

Lemmas

Notation

Operations

String (file)

Iter (file)

Basic

Intercalate

Lemmas (file)

Pattern (file)

Find (file)

Basic

Char

Pred

String

Split (file)

Basic

Char

Pred

String (file)

Basic

ForwardPattern

ForwardSearcher

TakeDrop (file)

Basic

Char

Pred

String

Basic

Char

Memcmp

Pred

Basic

FindPos

Hashable

Intercalate

IsEmpty

Iter

Iterate

Length

Modify

Order

Search

Slice

Splits

StringOrder

TakeDrop

Pattern (file)

Basic

Char

Pred

String

Basic

Bootstrap

Decode

Defs

Extra

FindPos

Hashable

Iterate

Iterator

Legacy

Length

Modify

OrderInstances

PosRaw

Search

Slice

Stream

Subslice

Substring

TakeDrop

Termination

ToSlice

Subtype (file)

Basic

Order

OrderExtra

Sum (file)

Basic

Lemmas

ToString (file)

Basic

Extra

Macro

Name

UInt (file)

Basic

BasicAux

Bitwise

Lemmas

Log2

Vector (file)

Algebra

Attach

Basic

Count

DecidableEq

Erase

Extract

FinRange

Find

InsertIdx

Int

Lemmas

Lex

MapIdx

Monadic

Nat

OfFn

Perm

Range

Stream

Zip

AC

BEq

Bool

Cast

Float

Float32

Function

Hashable

LawfulHashable

NeZero

OfScientific

PLift

Prod

Queue

RArray

Random

Repr

Stream

ULift

Zero

Grind (file)

Module (file)

Basic

Envelope

NatModuleNorm

OfNatModule

Ordered (file)

Field

Int

Linarith

Module

Order

Rat

Ring

Ring (file)

Basic

CommSemiringAdapter

CommSolver

Envelope

Field

OfScientific

ToInt

AC

Annotated

Attr

Cases

Config

Ext

FieldNormNum

Injective

Interactive

Lemmas

Lint

Norm

Offset

Order

PP

Propagator

Tactics

ToInt

ToIntLemmas

Util

GrindInstances (file)

Ring (file)

BitVec

Fin

Int

Nat

Rat

SInt

UInt

Nat

ToInt

Internal (file)

Order (file)

Basic

Lemmas

MonadTail

Tactic

While

Meta (file)

Defs

Omega (file)

Coeffs

Constraint

Int

IntList

LinearCombo

Logic

Sym (file)

DSimp

DSimprocDSL

Simp

SimprocDSL

Lemmas

System (file)

CancelToken

FilePath

IO

IOError

Platform

Promise

ST

Uri

BinderNameHint

BinderPredicates

ByCases

CbvSimproc

Classical

Coe

Conv

Core

Dynamic

Ext

GetElem

Guard

Hints

LawfulBEqTactics

MacroTrace

MetaTypes

MethodSpecsSimp

Notation

NotationExtra

Prelude

PropLemmas

RCases

ShareCommon

SimpLemmas

Simproc

SizeOf

SizeOfLemmas

Syntax

Tactics

TacticsExtra

Task

Try

Util

WF

WFComputable

WFExtrinsicFix

WFTactics

While

Lake (file)

Build (file)

Job (file)

Basic

Monad

Register

Target (file)

Basic

Fetch

Actions

Common

Context

Data

Executable

ExternLib

Facets

Fetch

Index

Info

Infos

InitFacets

InputFile

Key

Library

Module

ModuleArtifacts

Package

Run

Store

Targets

Topological

Trace

CLI

Actions

Config (file)

Artifact

Cache

ConfigDecl

ConfigTarget

Context

Defaults

Dependency

Dynlib

Env

ExternLib

ExternLibConfig

FacetConfig

Glob

InputFile

InputFileConfig

InstallPath

Kinds

LakeConfig

Lang

LeanConfig

LeanExe

LeanExeConfig

LeanLib

LeanLibConfig

Meta

MetaClasses

Module

Monad

Opaque

OutFormat

Package

PackageConfig

Pattern

Script

TargetConfig

Workspace

WorkspaceConfig

DSL (file)

Attributes

AttributesCore

Config

DeclUtil

Extensions

Key

Meta

Package

Require

Script

Syntax

Targets

VerLit

Toml (file)

Data (file)

DateTime

Dict

Value

Elab (file)

Expression

Value

Decode

Encode

Grammar

Load

ParserUtil

Util (file)

Binder

Casing

Cli

Cycle

Date

EStateT

EquipT

Error

Exit

Family

FilePath

Git

IO

JsonObject

Lift

Lock

Log

MainM

Message

Name

NativeLib

Opaque

OpaqueType

OrdHashSet

OrderedTagAttribute

Proc

RBArray

Reservoir

Store

StoreInsts

String

Task

Url

Version

Reservoir

Version

Lean (file)

Compiler (file)

IR (file)

Basic

Checker

CompilerM

EmitLLVM

EmitUtil

Format

LLVMBindings

Meta

NormIds

Sorry

ToIR

ToIRType

UnboxResult

LCNF (file)

Simp (file)

Basic

Config

ConstantFold

DefaultAlt

DiscrM

FunDeclInfo

InlineCandidate

InlineProj

JpCases

Main

SimpM

SimpValue

Used

AlphaEqv

AuxDeclCache

BaseTypes

Basic

Bind

CSE

Check

Closure

CoalesceRC

CompatibleTypes

CompilerM

ConfigOptions

DeclHash

DependsOn

ElimDead

ElimDeadBranches

EmitC

EmitUtil

ExpandResetReuse

ExplicitBoxing

ExplicitRC

ExtractClosed

FVarUtil

FixedParams

FloatLetIn

InferBorrow

InferType

Internalize

Irrelevant

JoinPoints

LCtx

LambdaLifting

Level

LiveVars

Main

MonadScope

MonoTypes

OtherDecl

PassManager

Passes

PhaseExt

PrettyPrinter

Probing

PropagateBorrow

PublicDeclsExt

PullFunDecls

PullLetDecls

PushProj

ReduceArity

ReduceJpArity

Renaming

ResetReuse

ScopeM

SimpCase

SimpleGroundExpr

SpecInfo

Specialize

SplitSCC

StructProjCases

ToDecl

ToExpr

ToImpure

ToImpureType

ToLCNF

ToMono

Toposort

Types

Util

Visibility

BorrowedAnnotation

CSimpAttr

ClosedTermCache

ExportAttr

ExternAttr

FFI

ImplementedByAttr

InitAttr

InlineAttrs

Main

MetaAttr

ModPkgExt

NameDemangling

NameMangling

NeverExtractAttr

NoncomputableAttr

Old

Options

Specialize

Data (file)

Iterators (file)

Producers (file)

PersistentHashMap

Json (file)

FromToJson (file)

Basic

Extra

Basic

Elab

Parser

Printer

Stream

Lsp (file)

Basic

BasicAux

CancelParams

Capabilities

Client

CodeActions

Communication

Diagnostics

Extra

InitShutdown

Internal

Ipc

LanguageFeatures

TextSync

Utf16

Window

Workspace

NameMap (file)

AdditionalOperations

Basic

Array

AssocList

DeclarationRange

EditDistance

Format

FuzzyMatching

JsonRpc

KVMap

LBool

LOption

Name

NameTrie

OpenDecl

Options

PPContext

PersistentArray

PersistentHashMap

PersistentHashSet

Position

PrefixTree

RArray

RBMap

RBTree

SMap

SSet

Trie

DocString (file)

Add

Extension

Formatter

Links

Markdown

Parser

Syntax

Types

Elab (file)

BuiltinDo (file)

Basic

For

Forward

If

Jump

Let

Match

MatchExpr

Misc

Repeat

TryCatch

Command (file)

Scope

WithWeakNamespace

ConfigEval (file)

Basic

Builtins

Commands

DeriveEvalConfigItem

DeriveEvalExpr

DeriveEvalTerm

Extra

Instances

MetaInstances

Types

Util

Deriving (file)

BEq

Basic

DecEq

FromToJson

Hashable

Inhabited

LawfulBEq

Nonempty

Ord

ReflBEq

Repr

SizeOf

ToExpr

TypeName

Util

Do (file)

Basic

Control

ForwardSyntax

InferControlInfo

Legacy

PatternVar

Switch

DocString (file)

Builtin (file)

Keywords

Parsing

Postponed

Scopes

InfoTree (file)

InlayHints

Main

Types

PreDefinition (file)

PartialFixpoint (file)

Eqns

Induction

Main

Structural (file)

BRecOn

Basic

Eqns

FindRecArg

IndGroupInfo

IndPred

Main

Preprocess

RecArgInfo

SmartUnfolding

WF (file)

Basic

Eqns

Fix

FloatRecApp

GuessLex

Main

PackMutual

Preprocess

Rel

Unfold

Basic

EqUnfold

Eqns

EqnsUtils

FixedParams

Main

MkInhabitant

Mutual

TerminationHint

TerminationMeasure

Quotation (file)

Precheck

Util

Tactic (file)

BVDecide (file)

BVCheck

BVDecide

BVTrace

Normalize

Conv (file)

Basic

Cbv

Change

Congr

Delta

Lets

Pattern

Rewrite

Simp

Unfold

Do (file)

Internal (file)

VCGen (file)

Context

Driver

Entails

Frontend

Reduce

RuleCache

RuleConstruction

Solve

SpecDB

Util

ProofMode (file)

Assumption

Basic

Cases

Clear

Constructor

Delab

Exact

Exfalso

Focus

Frame

Have

Intro

LeftRight

MGoal

Pure

Refine

RenameI

Revert

Specialize

VCGen (file)

Basic

Split

SuggestInvariant

Attr

LetElim

Spec

Syntax

Grind (file)

Anchor

Annotated

Basic

BuiltinTactic

Config

DSimprocDSL

DSimprocDSLBuiltin

Filter

Have

Lint

LintExceptions

Main

Param

RegisterSymDSimp

RegisterSymSimp

ShowState

SimprocDSL

SimprocDSLBuiltin

Sym

Trace

WithGrindTacticM

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

AsAuxLemma

Basic

BoolToPropSimps

BuiltinTactic

Calc

Cbv

CbvSimproc

Change

Classical

Config

Congr

Decide

Delta

DiscrTreeKey

Doc

ElabTerm

ExposeNames

Ext

FalseOrByContra

Generalize

Guard

Impossible

Induction

Injection

Lets

LibrarySearch

Location

Match

Meta

Monotonicity

NormCast

RCases

RenameInaccessibles

Repeat

Rewrite

Rewrites

Rfl

Show

ShowTerm

Simp

SimpArith

SimpTrace

Simpa

Simproc

SolveByElim

Split

Symm

TreeTacAttr

Try

Unfold

Term (file)

TermElabM

App

Arg

AssertExists

Attributes

AutoBound

AuxDef

BinderPredicates

Binders

BindersUtil

BuiltinCommand

BuiltinEvalCommand

BuiltinNotation

BuiltinTerm

Calc

CheckTactic

Coinductive

ComputedFields

Config

DeclModifiers

DeclNameGen

DeclUtil

Declaration

DeclarationRange

DefView

DeprecatedArg

DeprecatedSyntax

ElabRules

ErrorExplanation

ErrorUtils

Eval

Exception

Extra

Frontend

GenInjective

GuardMsgs

Idbg

Import

Inductive

InfoTrees

InheritDoc

LetRec

Level

Macro

MacroArgUtil

MacroRules

Match

MatchAltView

MatchExpr

Mixfix

MutualDef

MutualInductive

Notation

Open

Parallel

ParseImportsFast

PatternVar

Print

RecAppSyntax

RecommendedSpelling

SetOption

StructInst

StructInstHint

Structure

Syntax

SyntheticMVars

Task

Time

Util

WhereFinally

Language

Lean (file)

Types

Basic

Util

LibrarySuggestions (file)

Basic

Default

MePo

SineQuaNon

SymbolFrequency

Linter (file)

EnvLinter (file)

Basic

Frontend

Extra (file)

DupNamespace

UnnecessarySeqFocus

UnreachableTactic

UnusedDecidableInType

Basic

Builtin

CheckUnivs

Coe

ConstructorAsVariable

DefProp

Deprecated

DocsOnAlt

GlobalAttributeIn

Init

List

MissingDocs

Omit

PersistentLintLog

Sets

TacticTypeCheck

UnusedSimpArgs

UnusedVariables

Util

Meta (file)

ArgsPacker (file)

Basic

Constructions (file)

BRecOn

CasesOn

CasesOnSameCtor

CtorElim

CtorIdx

NoConfusion

RecOn

SparseCasesOn

SparseCasesOnEq

DiscrTree (file)

Basic

Main

Types

Util

Match (file)

MatcherApp (file)

Basic

Transform

AltTelescopes

Basic

CaseArraySizes

CaseValues

MVarRenaming

Match

MatchEqs

MatchEqsExt

MatchPatternAttr

MatcherInfo

NamedPatterns

Rewrite

SimpH

SolveOverlap

Value

Sym (file)

Arith (file)

Classify

DenoteExpr

EvalNum

Functions

MonadCanon

MonadRing

MonadSemiring

MonadVar

Poly

Reify

ToExpr

Types

VarRename

DSimp (file)

App

DSimpM

DSimproc

EvalGround

Forall

Lambda

Let

Main

Reduce

Result

Variant

Simp (file)

App

Attr

CongrInfo

ControlFlow

Debug

Discharger

DiscrTree

EvalGround

Forall

Goal

Have

Lambda

Main

RegisterCommand

Result

Rewrite

SimpM

Simproc

Telescope

Theorems

Variant

AbstractS

AlphaShareBuilder

AlphaShareCommon

Apply

Canon

Eta

ExprPtr

Grind

InferType

InstantiateMVarsS

InstantiateS

Intro

IsClass

LitValues

LooseBVarsS

MaxFVar

Offset

Pattern

ProofInstInfo

ReplaceS

SymM

SynthInstance

Util

Tactic (file)

AC (file)

Main

BVDecide (file)

LRAT (file)

Cert

Trim

Normalize (file)

AC

AndFlatten

ApplyControlFlow

Basic

EmbeddedConstraint

Enums

IntToBitVec

Rewrite

ShortCircuit

Simproc

Structures

TypeAnalysis

Prover (file)

Basic

Bitblast

Reflect (file)

Basic

ReifiedBVExpr

ReifiedBVLogical

ReifiedBVPred

ReifiedLemmas

Reify

SatAtBVLogical

Attr

Counterexample

External

Main

TacticContext

Cbv (file)

BuiltinCbvSimprocs

Array

Core

String

CbvEvalExt

CbvSimproc

ControlFlow

Main

Opaque

TheoremsLookup

Util

Grind (file)

AC (file)

Action

DenoteExpr

Eq

Internalize

Inv

PP

Proof

Seq

ToExpr

Types

Util

Var

VarRename

Arith (file)

CommRing (file)

Action

DenoteExpr

EqCnstr

Functions

Internalize

Inv

MonadRing

MonadSemiring

NonCommRingM

NonCommSemiringM

PP

Power

Proof

Reify

RingId

RingM

SafePoly

SemiringM

Types

Cutsat (file)

Action

CommRing

DvdCnstr

EqCnstr

Inv

LeCnstr

MBTC

Model

Nat

Norm

Proof

ReorderVars

Search

SearchM

ToInt

ToIntInfo

Types

Util

Var

VarRename

Linear (file)

Action

Den

DenoteExpr

IneqCnstr

Internalize

Inv

LinearM

MBTC

Model

OfNatModule

PP

Proof

PropagateEq

Reify

Search

SearchM

StructId

ToExpr

Types

Util

Var

VarRename

EvalNum

FieldNormNum

Insts

IsRelevant

Main

Model

ModelUtil

Propagate

Simproc

Types

Util

Order (file)

Assert

Internalize

OrderM

Proof

StructId

Types

Util

Action

Anchor

Attr

Beta

Cases

CasesMatch

CastLike

CheckResult

CollectParams

Core

Ctor

CtorIdx

Diseq

EMatch

EMatchAction

EMatchTheorem

EMatchTheoremParam

EMatchTheoremPtr

EqResolution

Ext

ExtAttr

Extension

Filter

Finish

ForallProp

Injection

Injective

Internalize

Intro

Inv

LawfulEqCmp

Lookahead

MBTC

Main

MarkNestedSubsingletons

MatchCond

MatchDiscrOnly

OrderInsts

PP

Parser

Proj

Proof

ProofUtil

Propagate

PropagateInj

PropagatorAttr

ProveEq

ReflCmp

RegisterCommand

RevertAll

Simp

SimpUtil

Solve

Split

SynthInstance

Theorems

Types

Util

VarRename

Simp (file)

Arith (file)

Int (file)

Basic

Simp

Nat (file)

Basic

Simp

Util

BuiltinSimprocs (file)

Array

BitVec

Char

Core

CtorIdx

Fin

Int

List

MethodSpecs

Nat

SInt

String

UInt

Util

Attr

Diagnostics

LoopProtection

Main

RegisterCommand

Rewrite

SimpAll

SimpCongrTheorems

SimpTheorems

Simproc

Types

Try (file)

Collect

Acyclic

Apply

Assert

Assumption

AuxLemma

Backtrack

Cases

CasesOnStuckLHS

Cleanup

Clear

Congr

Constructor

Contradiction

Delta

ElimInfo

ExposeNames

Ext

FVarSubst

FunInd

FunIndCollect

FunIndInfo

Generalize

IndependentOf

Induction

Injection

Intro

Lets

LibrarySearch

NormCast

Refl

Rename

Repeat

Replace

Revert

Rewrite

Rewrites

Rfl

SolveByElim

Split

SplitIf

Subst

Symm

TryThis

Unfold

UnifyEq

Util

ACLt

AbstractMVars

AbstractNestedProofs

AppBuilder

Basic

BinderNameHint

Canonicalizer

CasesInfo

Check

CheckTactic

Closure

Coe

CoeAttr

CollectFVars

CollectMVars

CompletionName

CongrTheorems

CtorIdxHInj

CtorRecognizer

DecLevel

Diagnostics

Eqns

Eval

ExprDefEq

ExprLens

ExprTraverse

ForEachExpr

FunInfo

GeneralizeTelescope

GeneralizeVars

GetUnfoldableConst

HasAssignableMVar

HasNotBit

HaveTelescope

Hint

IndPredBelow

Inductive

InferType

Injective

Instances

IntInstTesters

Iterator

KAbstract

KExprMap

LazyDiscrTree

LetToHave

LevelDefEq

LitValues

MatchUtil

MethodSpecs

MkIffOfInductiveProp

MonadSimp

NatInstTesters

NatTable

Native

Offset

Order

PPBinder

PPGoal

PProdN

ProdN

RecExt

RecursorInfo

Reduce

ReduceEval

SameCtorUtils

SizeOf

Sorry

SplitSparseCasesOn

StringLitProof

Structure

SynthInstance

Transform

TransparencyMode

TryThis

UnificationHint

WHNF

WrapInstance

Parser (file)

Module (file)

Syntax

Tactic (file)

Doc

Term (file)

Basic

Doc

Attr

Basic

Command

Do

Extension

Extra

Level

StrInterpolation

Syntax

Types

ParserCompiler (file)

Attribute

PrettyPrinter (file)

Delaborator (file)

Attributes

Basic

Builtins

DeclWithSig

FieldNotation

Metavariable

Options

SubExpr

TopDownAnalyze

Basic

Formatter

Parenthesizer

Server (file)

CodeActions (file)

Attr

Basic

Provider

UnknownIdentifier

Completion (file)

CompletionCollectors

CompletionInfoSelection

CompletionItemCompression

CompletionResolution

CompletionUtils

EligibleHeaderDecls

ImportCompletion

SyntheticCompletion

FileWorker (file)

ExampleHover

InlayHints

RequestHandling

SemanticHighlighting

SetupFile

SignatureHelp

Utils

WidgetRequests

Rpc (file)

Basic

Deriving

RequestHandling

Test (file)

Cancel

Refs

Runner

AsyncList

FileSource

GoTo

InfoUtils

Logging

ProtocolOverview

References

RequestCancellation

Requests

ServerTask

Snapshots

Utils

Watchdog

Util (file)

CollectAxioms

CollectFVars

CollectLevelMVars

CollectLevelParams

CollectLooseBVars

CollectMVars

Diff

FVarSubset

FindExpr

FindLevelMVar

FindMVar

FoldConsts

ForEachExpr

ForEachExprWhere

HasConstCache

Heartbeats

InstantiateLevelParams

LakePath

LeanOptions

MonadBacktrack

MonadCache

NumApps

NumObjs

OccursCheck

PPExt

ParamMinimizer

Path

Profile

Profiler

ProfilerServer

PtrSet

RecDepth

Recognizers

ReplaceExpr

ReplaceLevel

Reprove

SCC

SafeExponentiation

ShareCommon

Sorry

SortExprs

TestExtern

Trace

UnusedBinders

Widget (file)

Basic

Commands

Diff

InteractiveCode

InteractiveDiagnostic

InteractiveGoal

TaggedText

Types

UserWidget

AddDecl

Attributes

AutoDecl

AuxRecursor

BuiltinDocAttr

Class

CompactedRegion

CoreM

Declaration

DeclarationRange

DefEqAttrib

DeprecatedModule

EnvExtension

Environment

ErrorExplanation

Exception

Expr

ExtraModUses

HeadIndex

Hygiene

IdentifierSuggestion

ImportingFlag

InternalExceptionId

KeyedDeclsAttribute

LabelAttribute

Level

LoadDynlib

LocalContext

Log

Message

MetavarContext

Modifiers

MonadEnv

Namespace

OriginalConstKind

PrivateName

ProjFns

ReducibilityAttrs

Replay

ReservedNameAction

ResolveName

Runtime

ScopedEnvExtension

Setup

Shell

Structure

SubExpr

Syntax

ToExpr

ToLevel

LeanSearchClient (file)

Basic

LoogleSyntax

Syntax

MathFormalContract (file)

Cites

Discharges

Emit

RestateCheck

Mathlib

Algebra

Algebra

Spectrum

Basic

Pi

Quasispectrum

Subalgebra

Basic

Directed

IsSimpleOrder

Lattice

Operations

Pointwise

Prod

Tower

Basic

Bilinear

Defs

Epi

Equiv

Hom

IsSimpleRing

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Rat

RestrictScalars

Shrink

StrictPositivity

Tower

TransferInstance

Unitization

ZMod

BigOperators

Finsupp

Basic

Fin

Group

Finset

Basic

Defs

Indicator

Lemmas

Pi

Piecewise

Powerset

Preimage

Sigma

List

Basic

Defs

Lemmas

Multiset

Basic

Defs

GroupWithZero

Action

Finset

Ring

Finset

List

Multiset

Associated

Balance

Expect

Field

Fin

Finprod

Intervals

Module

NatAntidiagonal

Option

Pi

RingEquiv

WithTop

Category

AlgCat

Basic

TensorAlgebra

CommAlgCat

Basic

FiniteType

FGModuleCat

Abelian

Basic

Colimits

Limits

Grp

AB

Abelian

Adjunctions

Basic

Biproducts

Colimits

EpiMono

EquivalenceGroupAddGroup

FilteredColimits

ForgetCorepresentable

Injective

Kernels

LargeColimits

Limits

Preadditive

Ulift

Yoneda

ZModuleEquivalence

Zero

ModuleCat

Differentials

Basic

Presheaf

Monoidal

Basic

Closed

Symmetric

Presheaf (file)

Abelian

ChangeOfRings

ColimitFunctor

Colimits

EpiMono

Free

Generator

Limits

Monoidal

Pullback

Pushforward

Sheafification

Sheafify

Submodule

Sheaf (file)

Abelian

ChangeOfRings

Colimits

Free

Generators

Limits

Localization

LocallyFree

PullbackContinuous

PullbackFree

PushforwardContinuous

Quasicoherent

AB

Abelian

Adjunctions

Algebra

Basic

Biproducts

ChangeOfRings

ChangeOfRingsExact

Colimits

Descent

EpiMono

ExteriorPower

FilteredColimits

Injective

Kernels

LeftResolution

Limits

Localization

Products

Projective

Pseudofunctor

Semi

Simple

Stalk

Subobject

MonCat

Basic

FilteredColimits

ForgetCorepresentable

Limits

Ring

Under

Basic

Limits

Adjunctions

Basic

Colimits

Constructions

Epi

EqualizerPushout

FilteredColimits

Instances

Limits

LinearAlgebra

Small

Central

Basic

Defs

CharP

Algebra

Basic

CharAndCard

Defs

Frobenius

IntermediateField

Invertible

Lemmas

Reduced

Two

CharZero

AddMonoidHom

Defs

Infinite

Quotient

Colimit

DirectLimit

Finiteness

Module

TensorProduct

DirectSum

Algebra

Basic

Decomposition

Finsupp

Internal

Module

Ring

Divisibility

Basic

Hom

Units

EuclideanDomain

Basic

Defs

Field

Int

Exact

Basic

Sequence

Field

Subfield

Basic

Defs

Basic

Defs

Equiv

GeomSum

IsField

NegOnePow

Opposite

Periodic

Rat

TransferInstance

ZMod

FiniteSupport

Basic

Defs

FreeAbelianGroup

Finsupp

FreeMonoid

Basic

UniqueProds

GCDMonoid

Basic

Finset

IntegrallyClosed

Multiset

Nat

Group

Action

Pointwise

Set

Basic

Basic

Defs

End

Faithful

Hom

Opposite

Pi

Pretransitive

Prod

TransferInstance

TypeTags

Units

Commute

Basic

Defs

Hom

Units

Equiv

Basic

Defs

Opposite

TypeTags

Fin

Basic

Tuple

Hom

Basic

CompTypeclasses

Defs

End

Instances

Int

Defs

Even

Units

Invertible

Basic

Defs

Irreducible

Defs

Lemmas

Nat

Defs

Even

Hom

Range

Units

Pi

Basic

Lemmas

Units

Pointwise

Finset

Basic

Scalar

Set

Basic

BigOperators

Card

Finite

Lattice

ListOfFn

Scalar

Semiconj

Basic

Defs

Units

Subgroup

ZPowers

Basic

Lemmas

Actions

Basic

Defs

Finite

Ker

Lattice

Map

MulOpposite

MulOppositeLemmas

Order

Pointwise

Submonoid

Basic

BigOperators

Defs

DistribMulAction

Finite

Finsupp

Membership

MulAction

MulOpposite

Operations

Pointwise

Support

Units

Subsemigroup

Basic

Defs

Membership

MulOpposite

Operations

TypeTags

Basic

Finite

Hom

Pointwise

UniqueProds

Basic

Units

Basic

Defs

Equiv

Hom

Opposite

WithOne

Defs

Map

AddChar

Basic

Center

Commutator

Conj

Defs

Embedding

End

Even

EvenFunction

Ext

Finsupp

ForwardDiff

Graph

Idempotent

Indicator

InjSurj

MinimalAxioms

ModEq

Opposite

PUnit

Prod

Shrink

Support

Torsion

TransferInstance

ULift

GroupWithZero

Action

Pointwise

Set

Basic

Defs

End

Hom

Opposite

Pi

Prod

TransferInstance

Units

Pointwise

Set

Basic

Submonoid

Instances

Pointwise

Primal

Units

Basic

Equiv

Fintype

Lemmas

Associated

Basic

Center

Commute

Defs

Divisibility

Equiv

Hom

Idempotent

Indicator

InjSurj

Invertible

Nat

NeZero

NonZeroDivisors

Opposite

Pi

Prod

Range

Regular

Semiconj

Subgroup

ULift

WithZero

Homology

DerivedCategory

Ext

Basic

EnoughInjectives

EnoughProjectives

ExactSequences

ExtClass

Linear

Map

TStructure

Basic

DerivabilityStructureInjectives

ExactFunctor

Fractions

FullyFaithful

HomologySequence

KInjective

KProjective

Linear

Plus

RightDerivedFunctorPlus

ShortExact

SingleTriangle

SmallShiftedHom

TStructure

Embedding

AreComplementary

Basic

Boundary

CochainComplex

Extend

ExtendHomology

ExtendHomotopy

HomEquiv

IsSupported

Restriction

RestrictionHomology

StupidTrunc

TruncGE

TruncGEHomology

TruncLE

TruncLEHomology

Factorizations

Basic

CM5a

CM5b

HomotopyCategory (file)

Acyclic

DegreewiseSplit

HomComplex

HomComplexCohomology

HomComplexInduction

HomComplexShift

HomComplexSingle

HomologicalFunctor

KInjective

KProjective

MappingCocone

MappingCone

Plus

Pretriangulated

Shift

ShiftSequence

ShortExact

SingleFunctors

SpectralObject

Triangulated

LeftResolution

Basic

Reduced

Transport

ModelCategory

Injective

Lifting

ShortComplex

Ab

Abelian

Basic

ConcreteCategory

Exact

ExactFunctor

FunctorEquivalence

HomologicalComplex

Homology

LeftHomology

Limits

ModuleCat

Preadditive

PreservesHomology

QuasiIso

Retract

RightHomology

ShortExact

SnakeLemma

SpectralObject

Basic

Cycles

Differentials

EpiMono

FirstPage

HasSpectralSequence

Homology

Page

SpectralSequence

SpectralSequence

Basic

ComplexShape

Additive

Bifunctor

BifunctorAssociator

BifunctorFlip

CochainComplexOpposite

CochainComplexPlus

CommSq

ComplexShape

ComplexShapeSigns

ConcreteCategory

EulerCharacteristic

ExactSequence

ExactSequenceFour

FullSubcategory

HomologicalBicomplex

HomologicalComplex

HomologicalComplexAbelian

HomologicalComplexBiprod

HomologicalComplexLimits

HomologicalComplexLimitsEventuallyConstant

HomologySequence

HomologySequenceLemmas

Homotopy

HomotopyCofiber

HomotopyFiber

ImageToKernel

Linear

Localization

Monoidal

Opposite

Precylinder

QuasiIso

Refinements

Single

SingleHomology

Square

TotalComplex

TotalComplexShift

TotalComplexSymmetry

Module

Congruence

Defs

Equiv

Basic

Defs

Opposite

LinearMap

Basic

Defs

DivisionRing

End

Prod

Rat

Star

LocalizedModule

AtPrime

Away

Basic

Exact

Int

IsLocalization

Submodule

Presentation

Basic

Submodule

Basic

Bilinear

Defs

EqLocus

Equiv

Finsupp

Invariant

IterateMapComap

Ker

Lattice

LinearMap

Map

Pointwise

Range

RestrictScalars

Torsion

Basic

Field

Free

Pi

ZLattice

Basic

Basic

BigOperators

CharacterModule

Defs

End

FinitePresentation

GradedModule

Hom

Injective

MinimalAxioms

NatInt

Opposite

PUnit

Pi

Prod

Projective

Rat

RingHom

Shrink

SnakeLemma

SpanRank

SpanRankOperations

TransferInstance

ULift

ZMod

MonoidAlgebra

Basic

Defs

Degree

Division

Ideal

Lift

MapDomain

Module

NoZeroDivisors

Opposite

Support

MvPolynomial

Basic

CommRing

Degrees

Derivation

Division

Equiv

Eval

Monad

Nilpotent

NoZeroDivisors

PDeriv

Rename

Supported

Variables

NoZeroSMulDivisors

Basic

Defs

Notation (file)

Pi

Basic

Defs

Defs

FiniteSupport

Indicator

Lemmas

Prod

Support

Order

AbsoluteValue

Basic

Antidiag

Finsupp

Pi

Prod

Archimedean

Real

Basic

Basic

Defs

BigOperators

Group

Finset

List

LocallyFinite

Multiset

GroupWithZero

Finset

List

Multiset

Ring

Finset

List

Multiset

Expect

CauSeq

Basic

BigOperators

Completion

Field

Basic

Canonical

Power

Rat

Floor

Defs

Ring

Semiring

Group

Action (file)

Synonym

Pointwise

Bounds

CompleteLattice

Interval

Unbundled

Abs

Basic

Int

Abs

Basic

Cyclic

Defs

Finset

Indicator

Int

Lattice

MinMax

Multiset

Nat

Opposite

OrderIso

PiLex

PosPart

Synonym

Units

GroupWithZero

Action

Synonym

Basic

Canonical

Defs

Finset

OrderIso

Range

Submonoid

Synonym

WithZero

Hom

Basic

Monoid

MonoidWithZero

Ring

TypeTags

Units

Interval

Finset

Basic

SuccPred

Set

Group

Instances

Monoid

Module

Basic

Defs

Field

Pointwise

PositiveLinearMap

Rat

Synonym

Monoid

Canonical

Basic

Defs

Unbundled

Basic

Defs

ExistsOfLE

MinMax

OrderDual

Pow

TypeTags

WithTop

Basic

Defs

NatCast

OrderDual

Submonoid

TypeTags

Units

WithTop

Nonneg

Basic

Field

Floor

Lattice

Module

Ring

Positive

Ring

Ring

Unbundled

Basic

Rat

Abs

Basic

Canonical

Cast

Defs

Finset

GeomSum

Idempotent

InjSurj

Int

Interval

IsNonarchimedean

Nat

Pow

Rat

Star

Synonym

WithTop

Star

Basic

Prod

Real

Sub

Unbundled

Basic

Basic

Defs

WithTop

SuccPred (file)

PartialSups

WithBot

AddGroupWithTop

AddTorsor

Algebra

Invertible

IsBotOne

Kleene

Monovary

Pi

Round

ToIntervalMod

ZeroLEOne

Polynomial

Degree

Defs

Domain

Lemmas

Monomial

Operations

SmallDegree

Support

TrailingDegree

Units

Eval

Algebra

Coeff

Defs

Degree

SMul

Subring

Module

AEval

Basic

AlgebraMap

Basic

BigOperators

CancelLeads

Coeff

CoeffMem

Derivation

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Monic

Monomial

Reverse

RingDivision

Roots

Splits

Taylor

Prime

Defs

Lemmas

Regular

Basic

Defs

Opposite

Pow

SMul

Ring

Action

Pointwise

Set

Basic

ConjAct

End

Field

Group

Invariant

Rat

Submonoid

Subobjects

Divisibility

Basic

Hom

Defs

InjSurj

Int

Defs

Field

Parity

Units

Submonoid

Basic

Pointwise

Subring

Basic

Defs

Pointwise

Units

Subsemiring

Basic

Defs

Pointwise

AddAut

Associated

Associator

Aut

Basic

Center

Centralizer

CharZero

Commute

CompTypeclasses

Defs

Equiv

Fin

GeomSum

GrindInstances

Idempotent

InjSurj

Invertible

MinimalAxioms

Nat

NegOnePow

NonZeroDivisors

Opposite

PUnit

Parity

Periodic

Pi

Prod

Rat

Regular

Semiconj

Shrink

Torsion

TransferInstance

ULift

Units

Squarefree

Basic

Star

Basic

BigOperators

Center

Module

MonoidHom

NonUnitalSubalgebra

Pi

Pointwise

Prod

Rat

SelfAdjoint

StarAlgHom

StarProjection

StarRingHom

Subalgebra

TensorProduct

Unitary

UnitaryStarAlgAut

Torsor

Basic

Defs

TrivSqZeroExt

Basic

DualNumber

FiveLemma

FreeAlgebra

GradedMonoid

GradedMulAction

IsPrimePow

NeZero

Opposites

QuadraticDiscriminant

Quotient

AlgebraicGeometry

Cover

MorphismProperty

Open

Over

QuasiCompact

Sigma

Geometrically

Basic

Integral

Irreducible

Reduced

IdealSheaf

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

SchemeTheoreticallyDominant

Separated

Smooth

SurjectiveOnStalks

UnderlyingMap

UniversallyClosed

UniversallyOpen

ProjectiveSpectrum

Basic

Proper

Scheme

StructureSheaf

Topology

Sites

BigZariski

Etale

Fpqc

MorphismProperty

Pretopology

QuasiCompact

SheafQuasiCompact

Small

AffineScheme

AffineSpace

Artinian

EffectiveEpi

Fiber

FunctionField

GammaSpecAdjunction

Gluing

Limits

Noetherian

OpenImmersion

OrderOfVanishing

Over

Properties

PullbackCarrier

Pullbacks

ResidueField

Restrict

Scheme

Spec

Stalk

StructureSheaf

ValuativeCriterion

AlgebraicTopology

FundamentalGroupoid

Basic

FundamentalGroup

InducedMaps

PUnit

Product

SimplyConnected

ModelCategory

Basic

Bifibrant

BrownLemma

CategoryWithCofibrations

Cylinder

DerivabilityStructureFibrant

FibrantObjectHomotopy

Homotopy

Instances

IsCofibrant

LeftHomotopy

PathObject

RightHomotopy

RelativeCellComplex

AttachCells

Basic

SimplexCategory

Basic

Defs

DeltaZeroIter

Rev

Truncated

SimplicialObject

Basic

DeltaZeroIter

Homotopy

Op

SimplicialSet

Basic

CompStruct

CompStructTruncated

Degenerate

Dimension

Finite

Nerve

NerveNondegenerate

NonDegenerateSimplices

Op

Simplices

StdSimplex

Subcomplex

SubcomplexOp

AlternatingFaceMapComplex

CechNerve

ExtraDegeneracy

MooreComplex

Analysis

Analytic

Basic

CPolynomial

CPolynomialDef

ChangeOrigin

Composition

Constructions

ConvergenceRadius

Inverse

IsolatedZeros

Linear

OfScalars

RadiusLiminf

Uniqueness

Within

Asymptotics

AsymptoticEquivalent

Defs

Lemmas

TVS

Theta

BoxIntegral

Box

Basic

SubboxInduction

Partition

Additive

Basic

Filter

Measure

Split

SubboxInduction

Tagged

Basic

DivergenceTheorem

Integrability

CStarAlgebra

ContinuousFunctionalCalculus

Basic

Commute

Continuity

Instances

Isometric

NonUnital

Order

Pi

Restrict

Unique

Unital

Basic

Classes

ContinuousMap

Exponential

Fuglede

GelfandDuality

Matrix

Spectrum

Unitization

Calculus

ContDiff

Basic

Comp

Defs

Deriv

FTaylorSeries

FaaDiBruno

Operations

RCLike

WithLp

Deriv

Add

AffineMap

Basic

Comp

CompMul

Inv

Inverse

Linear

MeanValue

Mul

Polynomial

Pow

Shift

Slope

Support

ZPow

FDeriv

Add

Affine

Analytic

Basic

Bilinear

Comp

CompCLM

Congr

Const

Defs

Equiv

Linear

Measurable

Mul

OfCompLeft

Pow

Prod

RestrictScalars

WithLp

InverseFunctionTheorem

ApproximatesLinearOn

FDeriv

IteratedDeriv

Defs

Lemmas

LocalExtr

Basic

Rolle

TangentCone

Basic

Defs

DimOne

Prod

Real

DSlope

DiffContOnCl

FormalMultilinearSeries

LagrangeMultipliers

LogDeriv

MeanValue

Complex

Polynomial

Basic

Arg

Asymptotics

Basic

Cardinality

CauchyIntegral

Circle

Convex

Exponential

Liouville

Norm

Order

ReImTopology

RealDeriv

Spectrum

Trigonometric

Convex

Cone

Extension

SpecificFunctions

Basic

Deriv

Basic

Combination

Contractible

Deriv

EGauge

Function

Gauge

Hull

Jensen

Mul

PathConnected

Segment

Slope

Star

StdSimplex

Strict

StrictConvexSpace

Topology

TotallyBounded

Uniform

InnerProductSpace

Projection

Basic

FiniteDimensional

Minimal

Reflection

Submodule

Adjoint

Basic

Calculus

Continuous

Convex

Defs

Dual

GramSchmidtOrtho

LinearMap

Orientation

Orthogonal

Orthonormal

PiL2

ProdL2

Rayleigh

Spectrum

Subspace

Symmetric

LocallyConvex

AbsConvex

AbsConvexOpen

BalancedCoreHull

Barrelled

Basic

Bounded

HahnBanach

Polar

SeparatingDual

Separation

WeakDual

WithSeminorms

Matrix

Hermitian

HermitianFunctionalCalculus

Normed

Order

PosDef

Spectrum

Normed

Affine

AddTorsor

Isometry

Algebra

Basic

Exponential

GelfandFormula

Spectrum

Unitization

UnitizationL1

Field

Basic

Lemmas

UnitBall

Group

AddCircle

AddTorsor

BallSphere

Basic

Bounded

Completion

Constructions

Continuity

Defs

FunctionSeries

Hom

Indicator

InfiniteSum

Int

Lemmas

NullSubmodule

Pointwise

Quotient

Rat

Real

Seminorm

Subgroup

Submodule

Uniform

Lp

Matrix

MeasurableSpace

PiLp

ProdLp

WithLp

Module

Alternating

Basic

Ball

Homeomorph

Pointwise

Multilinear

Basic

Curry

RCLike

Basic

Extend

Real

Basic

Completion

Convex

Dual

FiniteDimension

HahnBanach

Ray

RieszLemma

Span

WeakDual

Operator

Compact

Basic

FiniteDimension

FredholmAlternative

Asymptotics

Banach

BanachSteinhaus

Basic

Bilinear

BoundedLinearMaps

CompleteCodomain

Completeness

ContinuousLinearMap

Extend

LinearIsometry

Mul

NNNorm

NormedSpace

Order

Lattice

Ring

Basic

Finite

InfiniteSum

Lemmas

Units

MulAction

RCLike

Basic

Extend

Lemmas

Sqrt

Real

Pi

Bounds

Cardinality

Spectrum

Sqrt

SpecialFunctions

Complex

Arg

Circle

CircleMap

Log

ContinuousFunctionalCalculus

PosPart

Basic

Rpow

Basic

Isometric

Abs

Log

Basic

Deriv

Pow

Asymptotics

Complex

Continuity

NNReal

Real

Trigonometric

Angle

Arctan

ArctanDeriv

Basic

Bounds

Complex

ComplexDeriv

Deriv

Inverse

Bernstein

Exp

ExpDeriv

Exponential

NonIntegrable

Sqrt

SpecificLimits

Basic

Normed

LConvolution

MeanInequalities

MeanInequalitiesPow

Oscillation

Seminorm

CategoryTheory

Abelian

DiagramLemmas

Four

KernelCokernelComp

GrothendieckAxioms

Basic

Colim

FunctorCategory

Sheaf

Types

GrothendieckCategory

Basic

ColimCoyoneda

EnoughInjectives

HasExt

Monomorphisms

Subobject

Injective

Ext

Extend

Resolution

Projective

Dimension

Extend

Resolution

SerreClass

Basic

Basic

CommSq

EpiWithInjectiveKernel

Exact

FunctorCategory

Images

LeftDerived

NonPreadditive

Opposite

Pseudoelements

Refinements

ShortExact

Subcategory

Subobject

Transfer

Adhesive

Basic

Adjunction

Additive

AdjointFunctorTheorems

Basic

Comma

CompositionIso

FullyFaithful

Limits

Mates

Opposites

Parametrized

PartialAdjoint

Reflective

Restrict

Unique

Whiskering

Bicategory

Adjunction

Adj

Basic

Cat

Mate

Functor

Cat (file)

ObjectProperty

Lax

LocallyDiscrete

Oplax

Prelax

Pseudofunctor

StrictPseudofunctor

StrictlyUnitary

FunctorBicategory

Pseudo

Modification

Oplax

Pseudo

NaturalTransformation

Oplax

Pseudo

Strict

Basic

Pseudofunctor

Basic

Free

LocallyDiscrete

Category

Cat (file)

AsSmall

Basic

Factorisation

GaloisConnection

Init

Pairwise

Preorder

Quiv

ULift

Center

Basic

Linear

Localization

NegOnePow

Preadditive

Comma

Over

Basic

OverClass

Pullback

Presheaf

Basic

StructuredArrow

Basic

Functor

Small

Arrow

Basic

CardinalArrow

CatCommSq

LocallySmall

ComposableArrows

Basic

Four

One

Three

Two

ConcreteCategory

Basic

Bundled

Elementwise

EpiMono

Forget

ReflectsIso

Representable

Discrete

Basic

StructuredArrow

EffectiveEpi

Basic

Comp

Preserves

Filtered

Basic

Connected

Final

FinallySmall

FinCategory

AsType

Basic

Functor

Derived

LeftDerived

PointwiseLeftDerived

PointwiseRightDerived

RightDerived

KanExtension

Adjunction

Basic

Pointwise

Preserves

ReflectsIso

Balanced

Basic

Exact

Jointly

Limits

Basic

Category

Const

Currying

EpiMono

Flat

FullyFaithful

Hom

OfSequence

Trifunctor

TwoSquare

Generator

Basic

Presheaf

Sheaf

GradedObject (file)

Associator

Bifunctor

Monoidal

Single

Trifunctor

Unitor

Groupoid (file)

Grpd

Basic

Discrete

GuitartExact

Basic

HorizontalComposition

KanExtension

Opposite

Quotient

VerticalComposition

Idempotents

Basic

FunctorCategories

FunctorExtension

Karoubi

LiftingProperties

Adjunction

Basic

Limits

Limits

ConcreteCategory

Basic

Filtered

Constructions

Over

Basic

Connected

Products

BinaryProducts

EpiMono

Equalizers

EventuallyConstant

Filtered

FiniteProductsOfBinaryProducts

LimitsOfProductsAndEqualizers

Pullbacks

WeaklyInitial

WidePullbackOfTerminal

ZeroObjects

Final (file)

Connected

Type

FormalCoproducts

Basic

Cech

ExtraDegeneracy

FunctorCategory

Shapes

Terminal

Basic

EpiMono

Finite

Preserves

Creates

Finite

Opposites

Pullbacks

Shapes

AbelianImages

BinaryProducts

Biproducts

Equalizers

Kernels

Preorder

Products

Pullbacks

Square

Terminal

Zero

Basic

Bifunctor

Filtered

Finite

FunctorCategory

Limits

Opposites

SigmaConst

Ulift

Shapes

NormalMono

Basic

Equalizers

Opposites

Equalizers

Filtered

Kernels

Products

Pullbacks

Preorder

Basic

Fin

HasIterationOfShape

PrincipalSeg

TransfiniteCompositionOfShape

WellOrderContinuous

Pullback

IsPullback

Basic

Defs

Kernels

Assoc

Cospan

Equalizer

Equifibered

HasPullback

Iso

Mono

Pasting

PullbackCone

Square

BinaryBiproducts

BinaryProducts

Biproducts

ConcreteCategory

Connected

Countable

Diagonal

DisjointCoproduct

Equalizers

Equivalence

FiniteLimits

FiniteProducts

Grothendieck

Images

IsTerminal

KernelPair

Kernels

Multiequalizer

Products

Reflexive

RegularMono

SplitCoequalizer

SplitEqualizer

StrictInitial

StrongEpi

Terminal

WideEqualizers

WidePullbacks

ZeroMorphisms

ZeroObjects

Types

Coequalizers

ColimitType

Colimits

Coproducts

Equalizers

Filtered

Images

Limits

Multiequalizer

Products

Pullbacks

Yoneda

Bicones

ColimitLimit

Comma

ConeCategory

Cones

Connected

Creates

Elements

EpiMono

EssentiallySmall

ExactFunctor

Filtered

FilteredColimitCommutesFiniteLimit

FinallySmall

Fubini

FullSubcategory

HasLimits

IsConnected

IsLimit

Lattice

MonoCoprod

MorphismProperty

Opposites

Over

Preorder

Presentation

Presheaf

Sifted

Skeleton

Unit

VanKampen

Yoneda

Linear

Basic

FunctorCategory

LinearFunctor

Yoneda

Localization

CalculusOfFractions (file)

ComposableArrows

Fractions

Preadditive

DerivabilityStructure

Basic

Constructor

Derives

OfLocalizedEquivalences

PointwiseRightDerived

Adjunction

Bifunctor

Bousfield

Composition

Construction

Equivalence

HasLocalization

HomEquiv

Linear

LocalizerMorphism

OfQuotient

Opposite

Predicate

Prod

Quotient

Resolution

SmallHom

SmallShiftedHom

StructuredArrow

Triangulated

Monad

Adjunction

Algebra

Basic

Comonadicity

Equalizer

Limits

Products

Monoidal

Braided

Basic

Cartesian

Basic

FunctorCategory

Mon

Over

Closed

Basic

Cartesian

Types

ExternalProduct

Basic

Free

Basic

Limits

Colimits

Preserves

Rigid

Basic

Types

Basic

Category

CoherenceLemmas

CommMon_

Discrete

End

Functor

FunctorCategory

Grp

Linear

Mon

NaturalTransformation

Opposite

Preadditive

Skeleton

Subcategory

Tor

Transport

MorphismProperty

Basic

Comma

Composition

Concrete

Factorization

IsInvertedBy

IsSmall

LiftingProperty

Limits

Local

OfObjectProperty

OverAdjunction

Quotient

Retract

RetractArgument

TransfiniteComposition

WeakFactorizationSystem

ObjectProperty

Basic

ClosedUnderIsomorphisms

ClosureShift

ColimitsClosure

ColimitsOfShape

CompleteLattice

ContainsZero

EpiMono

Equivalence

Extensions

FiniteProducts

FullSubcategory

Kernels

LimitsClosure

LimitsOfShape

Local

Opposite

Orthogonal

Retract

Shift

ShiftAdditive

Small

PathCategory

Basic

MorphismProperty

Pi

Basic

Preadditive

Injective

Basic

InjectiveObject

LiftingProperties

Preserves

Resolution

Projective

Basic

Preserves

Resolution

Yoneda

Basic

AdditiveFunctor

Basic

Biproducts

FunctorCategory

LeftExact

Opposite

Transfer

Presentable

IsCardinalFiltered

Products

Associator

Basic

Bifunctor

Unitor

Quotient (file)

Linear

Preadditive

Shift

Adjunction

Basic

CommShift

CommShiftTwo

Induced

InducedShiftSequence

Linear

Localization

Opposite

Pullback

Quotient

ShiftSequence

ShiftedHom

ShiftedHomOpposite

SingleFunctors

SingleFunctorsLift

Twist

Sites

CoversTop

Basic

Over

DenseSubsite

Basic

InducedTopology

SheafEquiv

Descent

DescentData

IsPrestack

IsStack

Precoverage

Hypercover

IsSheaf

One

SheafOfTypes

Zero

ZeroFamily

Point

Basic

SheafCohomology

Basic

Cech

MayerVietoris

Abelian

Adjunction

Canonical

Closed

CompatiblePlus

CompatibleSheafification

ConcreteSheafification

ConstantSheaf

Continuous

CoproductSheafCondition

CoverLifting

CoverPreserving

Coverage

EffectiveEpimorphic

EpiMono

EqualizerSheafCondition

Equivalence

GlobalSections

Grothendieck

InducedTopology

IsSheafFor

JointlySurjective

LeftExact

Limits

Localization

LocallyBijective

LocallyFullyFaithful

LocallyInjective

LocallySurjective

MayerVietorisSquare

MorphismProperty

Over

Plus

Precoverage

PrecoverageToGrothendieck

Preserves

PreservesLocallyBijective

PreservesSheafification

Pretopology

Pullback

Sheaf

SheafOfTypes

Sheafification

Sieves

Spaces

SubcanonicalOver

Subsheaf

Whiskering

SmallObject

Iteration

Basic

ExtendToSucc

FunctorOfCocone

Nonempty

Basic

Construction

IsCardinalForSmallObjectArgument

TransfiniteCompositionLifting

TransfiniteIteration

WellOrderInductionData

Subfunctor

Basic

Image

OfSection

Sieves

Subobject

ArtinianObject

Basic

Comma

FactorThru

HasCardinalLT

Lattice

Limits

MonoOver

NoetherianObject

WellPowered

Triangulated

Opposite

Basic

Functor

Pretriangulated

Subcategory

Triangle

Triangulated

TStructure

AbelianSubcategory

Basic

Heart

Induced

TruncLEGT

TruncLTGE

Adjunction

Basic

Functor

Generators

HomologicalFunctor

LocalizingSubcategory

Orthogonal

Pretriangulated

Rotate

SpectralObject

Subcategory

TriangleShift

Triangulated

Yoneda

Types

Basic

WithTerminal

Basic

Cone

Balanced

CatCommSq

CommSq

Conj

Core

Countable

Elements

Elementwise

Endomorphism

EpiMono

EqToHom

Equivalence

EssentialImage

EssentiallySmall

Extensive

FintypeCat

GlueData

Grothendieck

HomCongr

InducedCategory

IsConnected

Iso

IsomorphismClasses

LocallyDirected

NatIso

NatTrans

Noetherian

Opposites

PEmpty

PUnit

Retract

ShrinkYoneda

Simple

SingleObj

Skeletal

Square

Thin

Whiskering

Yoneda

Combinatorics

Enumerative

Partition

Basic

Composition

InclusionExclusion

Matroid

Minor

Restrict

Rank

Cardinal

ENat

Finite

Basic

Circuit

Closure

Constructions

Dual

IndepAxioms

Init

Loop

Map

Quiver

Basic

Cast

Path

Prefunctor

Push

SingleObj

Symmetric

Control

Monad

Basic

Traversable

Basic

Lemmas

Applicative

Basic

Bifunctor

Combinators

EquivFunctor

Functor

ULift

Data

Bool

Basic

Set

Complex

Basic

BigOperators

Countable

Basic

Defs

Small

DFinsupp

BigOperators

Defs

Encodable

Ext

Lex

Module

NeLocus

Order

Sigma

Small

Submonoid

WellFounded

ENNReal

Action

Basic

BigOperators

Holder

Inv

Lemmas

Operations

Real

ENat

Basic

Defs

Lattice

Pow

EReal

Basic

Inv

Operations

Fin

Tuple

Basic

NatAntidiagonal

Reflection

Sort

Basic

Embedding

Rev

SuccPred

SuccPredOrder

VecNotation

Finite

Defs

Prod

Set

Sigma

Sum

Finset

Lattice

Basic

Fold

Lemmas

Prod

Union

Attach

Attr

Basic

BooleanAlgebra

Card

Dedup

Defs

Density

Disjoint

Empty

Erase

Filter

Fin

Fold

Image

Insert

Max

NAry

NatAntidiagonal

NoncommProd

Option

Order

Pi

Piecewise

Powerset

Preimage

Prod

Range

SDiff

Sigma

Sort

Sum

Sym

SymmDiff

Union

Update

Finsupp

MonomialOrder (file)

DegLex

Antidiagonal

Basic

Defs

Encodable

Ext

Fin

Fintype

Indicator

Lex

Multiset

Option

Order

SMul

SMulWithZero

Single

ToDFinsupp

Weight

WellFounded

Fintype

Basic

BigOperators

Card

CardEmbedding

Defs

EquivFin

Fin

Inv

Lattice

List

OfMap

Option

Order

Parity

Perm

Pi

Pigeonhole

Powerset

Prod

Quotient

Sets

Shrink

Sigma

Sort

Sum

Vector

FunLike

Basic

Embedding

Equiv

Graded

Group

IsApply

Module

Ring

Int

Cast

Basic

Defs

Field

Lemmas

Pi

Prod

Order

Basic

Units

Basic

CharZero

ConditionallyCompleteOrder

DivMod

GCD

Init

Interval

LeastGreatest

ModEq

Notation

Range

Sqrt

SuccPred

WithZero

List

Perm

Basic

Lattice

Subperm

Basic

Chain

Count

Cycle

Dedup

Defs

Destutter

Duplicate

Enum

FinRange

Find

Flatten

Forall2

Induction

Infix

InsertIdx

Iterate

Lattice

Lex

MinMax

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

OffDiag

Pairwise

Permutation

Pi

Prime

ProdSigma

Range

Rotate

Sort

Sublists

Sym

TFAE

TakeDrop

Zip

Matrix

Basic

Basis

Block

Composition

Diagonal

Mul

Reflection

Multiset

AddSub

Antidiagonal

Basic

Bind

Count

Dedup

Defs

Filter

Find

FinsetOps

Fintype

Fold

Lattice

MapFold

NatAntidiagonal

OrderedMonoid

Pi

Powerset

Range

Replicate

Sections

Sort

Sum

Sym

UnionInter

ZeroCons

NNRat

Defs

Order

NNReal

Basic

Defs

Star

Nat

Cast

Order

Basic

Field

Ring

Basic

Commute

Defs

Field

NeZero

Prod

WithTop

Choose

Basic

Bounds

Cast

Central

Factorization

Sum

Vandermonde

Digits

Defs

Lemmas

Factorial

Basic

BigOperators

Cast

SuperFactorial

Factorization

Basic

Defs

Induction

LCM

PrimePow

Fib

Basic

GCD

Basic

BigOperators

NthRoot

Defs

Order

Lemmas

Prime

Basic

Defs

Infinite

Int

Pow

Basic

BinaryRec

Bits

Count

DvdSequence

Factors

Find

Init

Log

MaxPowDiv

ModEq

Multiplicity

Notation

Pairing

Periodic

PrimeFin

Set

Sqrt

Squarefree

SuccPred

Totient

WithBot

Option

Basic

Defs

NAry

Ordering

Basic

PNat

Basic

Defs

Equiv

Notation

Prime

Prod

Basic

Lex

PProd

TProd

Rat

Cast

CharZero

Defs

Lemmas

Order

BigOperators

Defs

Encodable

Floor

Init

Lemmas

Sqrt

Real

Basic

ConjExponents

ENatENNReal

Pointwise

Star

Rel (file)

Cover

Separated

Seq

Basic

Computation

Defs

Set

Finite

Basic

Lattice

Lemmas

Powerset

Range

Lattice (file)

Image

Pairwise

Basic

Lattice

List

Basic

BoolIndicator

BooleanAlgebra

Card

CoeSort

Constructions

Countable

Defs

Disjoint

Function

Functor

Image

Inclusion

Insert

List

MemPartition

Monotone

NAry

Notation

Operations

Order

Piecewise

PowersetCard

Prod

Restrict

Semiring

Sigma

Subset

Subsingleton

SymmDiff

UnionLift

SetLike

Basic

Fintype

Setoid

Basic

Sigma

Basic

Lex

Sign

Basic

Defs

Stream

Defs

Init

String

Defs

Sum

Basic

Order

Sym

Sym2 (file)

Init

Basic

Tree

Basic

Vector

Basic

Defs

W

Basic

Cardinal

ZMod

Aut

Basic

Defs

IntUnitsPower

QuotientGroup

Units

ValMinAbs

Bracket

Bundle

Ineq

Opposite

Part

Quot

SProd

Subtype

ULift

Dynamics

Ergodic

MeasurePreserving

FixedPoints

Basic

Defs

Topology

PeriodicPts

Defs

Lemmas

Minimal

FieldTheory

Finite

Basic

GaloisField

Trace

Galois

Abelian

Basic

GaloisClosure

Infinite

Notation

IntermediateField

Adjoin

Algebra

Basic

Defs

Algebraic

Basic

IsAlgClosed

AlgebraicClosure

Basic

Spectrum

Minpoly

Basic

Field

Finite

IsIntegrallyClosed

MinpolyDiv

Normal

Basic

Closure

Defs

PurelyInseparable

Basic

RatFunc

AsPolynomial

Basic

Defs

SplittingField

Construction

IsSplittingField

AlgebraicClosure

Extension

Finiteness

Fixed

IsSepClosed

KrullTopology

KummerPolynomial

Perfect

PolynomialGaloisGroup

PrimitiveElement

Separable

SeparableClosure

SeparableDegree

SeparablyGenerated

Tower

Geometry

Convex

Cone

Basic

Pointed

RingedSpace

LocallyRingedSpace (file)

HasColimits

ResidueField

PresheafedSpace (file)

Gluing

HasColimits

Basic

OpenImmersion

SheafedSpace

Stalks

GroupTheory

Abelianization

Defs

Commutator

Basic

Congruence

Basic

BigOperators

Defs

Hom

Opposite

Coset

Basic

Card

Defs

FreeGroup

Basic

GroupAction

DomAct

Basic

SubMulAction (file)

Pointwise

Basic

ConjAct

Defs

FixedPoints

FixingSubgroup

Hom

IterateAct

Pointwise

Quotient

Ring

MonoidLocalization

Away

Basic

Divisibility

Maps

MonoidWithZero

OreLocalization

Basic

OreSet

Perm

Cycle

Basic

Factors

Type

Basic

Closure

Fin

Finite

List

Option

Sign

Support

ViaEmbedding

QuotientGroup

Basic

Defs

Finite

ModEq

SpecificGroups

Cyclic (file)

Basic

Subgroup

Center

Centralizer

Saturated

Simple

Submonoid

Center

Centralizer

Inverses

Subsemigroup

Center

Centralizer

Archimedean

Complement

DedekindFinite

Divisible

Exponent

Finiteness

FreeAbelianGroup

Index

NoncommPiCoprod

OrderOfElement

PGroup

Rank

Solvable

Sylow

Torsion

Lean

Elab

Tactic

Meta

InfoTree

Term

Expr

Basic

ExtraRecognizers

Rat

MessageData

Trace

Meta (file)

RefinedDiscrTree (file)

Basic

Encode

Initialize

Lookup

Tactic

Rewrite

Basic

CongrTheorems

KAbstractPositions

Simp

PrettyPrinter

Delaborator

ContextInfo

Environment

FoldEnvironment

GoalsLocation

Linter

Name

LinearAlgebra

AffineSpace

AffineSubspace

Basic

Defs

Simplex

Basic

AffineEquiv

AffineMap

Basis

Centroid

Combination

Defs

Independent

Midpoint

Ordered

Pointwise

Restrict

Slope

Alternating

Basic

Curry

Basis

Basic

Bilinear

Cardinality

Defs

Exact

Fin

Prod

SMul

Submodule

VectorSpace

BilinearForm

Basic

DualLattice

Hom

Isometry

IsometryEquiv

Orthogonal

Properties

TensorProduct

Charpoly

BaseChange

Basic

ToMatrix

CliffordAlgebra

Basic

Conjugation

Fold

Grading

Complex

FiniteDimensional

Module

Dimension

Basic

Constructions

DivisionRing

ErdosKaplansky

Finite

Finrank

Free

FreeAndStrongRankCondition

LinearMap

Localization

OrzechProperty

RankNullity

StrongRankCondition

Subsingleton

DirectSum

Finite

Finsupp

TensorProduct

Dual

Basis

Defs

Lemmas

Eigenspace

Basic

Charpoly

ContinuousLinearMap

Matrix

Minpoly

Zero

ExteriorAlgebra

Basic

OfAlternating

ExteriorPower

Basic

Basis

Pairing

FiniteDimensional

Basic

Defs

Lemmas

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

Matrix

Basic

PID

StrongRankCondition

GeneralLinearGroup

AlgEquiv

Basic

LinearIndependent

Basic

Defs

Lemmas

Matrix

Charpoly

Basic

Coeff

Disc

Eigs

LinearMap

Minpoly

Determinant

Basic

Bird

GeneralLinearGroup

Defs

FinTwo

Action

Adjugate

Basis

BilinearForm

Block

ConjTranspose

Defs

Diagonal

DotProduct

Dual

Hadamard

Hermitian

Ideal

InvariantBasisNumber

Invertible

Kronecker

MvPolynomial

Nondegenerate

NonsingularInverse

Notation

Polynomial

PosDef

Rank

Reindex

RowCol

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

StdBasis

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

Vec

ZPow

Multilinear

Basic

Basis

Curry

DFinsupp

Finsupp

TensorProduct

PerfectPairing

Basic

PiTensorProduct

Basic

QuadraticForm

Basic

Isometry

IsometryEquiv

Radical

Real

Signature

Quotient

Basic

Bilinear

Card

Defs

SModEq

Basic

Pointwise

SesquilinearForm

Basic

Orthogonal

Span

Basic

Defs

TensorAlgebra

Basic

TensorPower

Basic

Pairing

TensorProduct

Associator

Basic

Basis

Defs

DirectLimit

Finiteness

Map

Pi

Prod

Quotient

RightExactness

Tower

Vanishing

BilinearMap

Coevaluation

Contraction

Countable

DFinsupp

Determinant

InvariantBasisNumber

Isomorphisms

Lagrange

LinearPMap

Orientation

Pi

Prod

Projection

Ray

StdBasis

Trace

UnitaryGroup

Vandermonde

Logic

Embedding

Basic

Set

Encodable

Basic

Lattice

Pi

Equiv

Fin

Basic

Rotate

Basic

Defs

Embedding

Finset

Fintype

Functor

List

Multiset

Nat

Option

PartialEquiv

Prod

Set

Sum

Function

Basic

Coequalizer

CompTypeclasses

Conjugate

Defs

DependsOn

Iterate

ULift

IsEmpty

Basic

Defs

Nontrivial

Basic

Defs

Small

Basic

Defs

List

Set

Basic

Denumerable

ExistsUnique

Lemmas

Nonempty

OpClass

Pairwise

Relation

Relator

Unique

UnivLE

MeasureTheory

Constructions

BorelSpace

Basic

Complex

ContinuousLinearMap

Metric

Metrizable

Order

Real

Polish

Basic

StronglyMeasurable

Pi

Function

L1Space

AEEqFun

HasFiniteIntegral

Integrable

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

Defs

Indicator

Monotonicity

Prod

SMul

TriangleInequality

LpSpace

Basic

Complete

Indicator

SpecialFunctions

Basic

StronglyMeasurable

AEStronglyMeasurable

Basic

Lemmas

AEEqFun

AEMeasurableSequence

ConvergenceInMeasure

Egorov

EssSup

LocallyIntegrable

LpOrder

SimpleFunc

SimpleFuncDense

SimpleFuncDenseLp

Group

Action

Arithmetic

Convolution

Defs

FundamentalDomain

LIntegral

MeasurableEquiv

Measure

Pointwise

Prod

Integral

Bochner

Basic

ContinuousLinearMap

FundThmCalculus

L1

Set

SumMeasure

VitaliCaratheodory

IntervalIntegral

Basic

FundThmCalculus

Periodic

Lebesgue

Add

Basic

Countable

DominatedConvergence

Map

Markov

Norm

Sub

CircleIntegral

DivergenceTheorem

DominatedConvergence

FinMeasAdditive

IntegrableOn

Marginal

MeanInequalities

Prod

SetToL1

MeasurableSpace

Basic

Constructions

CountablyGenerated

Defs

Embedding

EventuallyMeasurable

Instances

MeasurablyGenerated

Pi

Prod

Measure

Decomposition

Exhaustion

Haar

Basic

InnerProductSpace

OfBasis

Quotient

Lebesgue

Basic

Complex

EqHaar

Typeclasses

Finite

NullSingletonClass

Probability

SFinite

AEDisjoint

AEMeasurable

AbsolutelyContinuous

Comap

Content

Count

Dirac

Doubling

GiryMonad

Map

MeasureSpace

MeasureSpaceDef

MutuallySingular

NullMeasurable

OpenPos

Prod

QuasiMeasurePreserving

Real

Regular

Restrict

Stieltjes

Trim

WithDensity

Order

Lattice

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfFunction

Operations

PiSystem

Topology

NumberTheory

ArithmeticFunction

Defs

Misc

Moebius

Zeta

Cyclotomic

Basic

PrimitiveRoots

LegendreSymbol

QuadraticChar

Basic

GaussSum

AddCharacter

Basic

JacobiSymbol

QuadraticReciprocity

ZModChar

MulChar

Basic

Lemmas

NumberField

Basic

Padics

PadicVal

Basic

Defs

Real

Irrational

Divisors

GaussSum

Order

Atoms (file)

Finite

BooleanAlgebra

Basic

Defs

Set

BoundedOrder

Basic

Lattice

Monotone

Bounds

Basic

Defs

Image

OrderIso

Category

FinPartOrd

Lat

LinOrd

NonemptyFinLinOrd

PartOrd

Preord

CompactlyGenerated

Basic

Intervals

CompleteLattice

Basic

Chain

Defs

Finset

Group

Lemmas

ConditionallyCompleteLattice

Basic

Defs

Finset

Group

Indexed

ConditionallyCompletePartialOrder

Basic

Defs

Indexed

Defs

LinearOrder

PartialOrder

Prop

Unbundled

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

Ultrafilter

Basic

Defs

Basic

Cofinite

CountableInter

CountableSeparatingOn

CountablyGenerated

Curry

Defs

ENNReal

EventuallyConst

Extr

Finite

IndicatorFunction

Interval

IsBounded

Ker

Lift

Map

NAry

Pi

Pointwise

Prod

SmallSets

Subsingleton

Tendsto

TendstoCofinite

Fin

Basic

Clamp

Finset

SuccAboveOrderIso

Tuple

GaloisConnection

Basic

Defs

Heyting

Basic

Boundary

Hom

Hom

Basic

Bounded

BoundedLattice

CompleteLattice

Lattice

Lex

Order

PowersetCard

Set

WithTopBot

Interval

Finset

Basic

Defs

Fin

Nat

SuccPred

Set

Basic

Defs

Disjoint

Fin

Final

Image

Infinite

InitialSeg

Limit

LinearOrder

Monotone

OrdConnected

OrdConnectedComponent

OrderEmbedding

OrderIso

Pi

ProjIcc

SuccOrder

SuccPred

UnorderedInterval

WithBotTop

Multiset

Lattice (file)

Nat

Monotone

Basic

Defs

Monovary

Preorder

Chain

Finite

Finsupp

RelIso

Basic

Set

SuccPred

Archimedean

Basic

CompleteLinearOrder

InitialSeg

Limit

LinearLocallyFinite

Relation

WithBot

UpperLower

Basic

Closure

CompleteLattice

Fibration

Principal

Antichain

Antisymmetrization

Basic

BooleanSubalgebra

BourbakiWitt

Circular

Closure

Cofinal

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

Copy

Cover

DirSupClosed

Directed

DirectedInverseSystem

Disjoint

Disjointed

FixedPoints

GameAdd

Ideal

InitialSeg

IsNormal

Iterate

JordanHolder

KrullDimension

LatticeIntervals

Lex

LiminfLimsup

Max

MinMax

Minimal

ModularLattice

Nat

Notation

OmegaCompletePartialOrder

OrdContinuous

OrderDual

OrderIsoNat

Part

PartialSups

PiLex

PropInstances

RelClasses

RelSeries

ScottContinuity

SetAccumulate

SetDissipate

SetIsMax

SetNotation

Shrink

Sublattice

SupClosed

SupIndep

SymmDiff

TransfiniteIteration

TypeTags

ULift

WellFounded

WellFoundedSet

WellQuasiOrder

WithBot

WithBotTop

Zorn

ZornAtoms

Probability

ConditionalProbability

UniformOn

RingTheory

AdicCompletion

Algebra

AsTensorProduct

Basic

Exactness

Functoriality

Adjoin

Polynomial

Basic

Basic

Dimension

FG

FGBaseChange

Field

PowerBasis

Singleton

Tower

Algebraic

Basic

Defs

Integral

MvPolynomial

AlgebraicIndependent

Adjoin

AlgebraicClosure

Basic

Defs

TranscendenceBasis

Transcendental

Artinian

Defs

Module

Ring

Congruence

Basic

Defs

Hom

Opposite

Coprime

Basic

Ideal

Lemmas

DedekindDomain

Ideal

Basic

Lemmas

AdicValuation

Basic

Dvr

IntegralClosure

Derivation

Basic

ToSquareZero

DiscreteValuationRing

Basic

TFAE

Etale

Basic

Field

Kaehler

Locus

Pi

Extension

Cotangent

Basic

Basis

Free

LocalizationAway

Presentation

Basic

Core

Submersive

Basic

Generators

Finiteness

Basic

Bilinear

Cardinality

Cofinite

Defs

FinitePresentationLocal

FiniteTypeLocal

Finsupp

Ideal

Lattice

Nakayama

Prod

Projective

Small

Subalgebra

Flat

FaithfullyFlat

Algebra

Basic

Basic

CategoryTheory

Equalizer

EquationalCriterion

Localization

Stability

Tensor

TorsionFree

FractionalIdeal

Basic

Inverse

Operations

GradedAlgebra

Homogeneous

Ideal

Submodule

Basic

FiniteType

HomogeneousLocalization

Radical

RingHom

Ideal

MinimalPrime

Basic

Localization

Noetherian

Quotient

Basic

ChineseRemainder

Defs

Nilpotent

Noetherian

Operations

PowTransition

Basic

BigOperators

Colon

Cotangent

Defs

GoingDown

GoingUp

Height

IdempotentFG

IsPrimary

IsPrincipal

KrullsHeightTheorem

Lattice

Maps

Maximal

Nonunits

Oka

Operations

Over

Pointwise

Prime

Prod

Span

Int

Basic

IntegralClosure

Algebra

Basic

Defs

IsIntegral

Basic

Defs

IsIntegralClosure

Basic

Defs

IntegrallyClosed

Jacobson

Ideal

Polynomial

Radical

Ring

Semiprimary

Kaehler

Basic

JacobiZariski

Polynomial

TensorProduct

KrullDimension

Basic

Field

NonZeroDivisors

PID

Zero

LocalProperties

Basic

Exactness

IntegrallyClosed

Projective

ProjectiveDimension

Reduced

Submodule

LocalRing

MaximalIdeal

Basic

Defs

ResidueField

Basic

Defs

Fiber

Ideal

RingHom

Basic

Basic

Defs

LocalSubring

Module

Localization

AtPrime

Basic

Away

AdjoinRoot

Basic

Lemmas

Algebra

AsSubring

BaseChange

Basic

Defs

Finiteness

FractionRing

Free

Ideal

Integer

Integral

InvSubmonoid

LocalizationLocalization

Module

NumDen

Submodule

MvPolynomial

MonomialOrder (file)

DegLex

Symmetric

Defs

Basic

Homogeneous

Ideal

Localization

Tower

WeightedHomogeneous

MvPowerSeries

Basic

LexOrder

NoZeroDivisors

Order

Nilpotent

Basic

Defs

Lemmas

Noetherian

Basic

Defs

Nilpotent

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Basic

Defs

Transitivity

OrderOfVanishing

Basic

Noetherian

OreLocalization

Basic

NonZeroDivisors

OreSet

Ring

Polynomial

Cyclotomic

Basic

Eval

Expand

Roots

Eisenstein

Basic

Criterion

Resultant

Basic

Basic

Bernstein

Content

DegreeLT

GaussLemma

Ideal

IntegralNormalization

Nilpotent

Pochhammer

Quotient

RationalRoot

ScaleRoots

SeparableDegree

Subring

Tower

UniqueFactorization

Vieta

PowerSeries

Basic

RegularLocalRing

Defs

RingHom

EssFiniteType

Etale

FaithfullyFlat

Finite

FinitePresentation

FiniteType

Flat

Injective

Integral

Locally

LocallyStandardSmooth

Smooth

StandardSmooth

Surjective

Unramified

RootsOfUnity

Basic

Complex

Minpoly

PrimitiveRoots

SimpleModule

Basic

Rank

SimpleRing

Basic

Defs

Matrix

Smooth

AdicCompletion

Basic

Fiber

Field

Flat

Kaehler

Local

Locus

NoetherianDescent

Pi

StandardSmooth

StandardSmoothCotangent

StandardSmoothOfFree

Spectrum

Maximal

Basic

Defs

Localization

Prime

Basic

Chevalley

ChevalleyComplexity

ConstructibleSet

Defs

FreeLocus

Jacobson

Noetherian

Polynomial

RingHom

TensorProduct

Topology

TensorProduct

Basic

Finite

Free

IncludeLeftSubRight

IsBaseChangePi

Maps

MonoidAlgebra

MvPolynomial

Pi

Quotient

Trace

Basic

Defs

TwoSidedIdeal

Basic

Kernel

Lattice

Operations

UniqueFactorizationDomain

Basic

Defs

FactorSet

Finite

GCDMonoid

Ideal

Multiplicity

Nat

NormalizedFactors

Unramified

Basic

Field

Finite

LocalRing

Locus

Pi

Valuation

Discrete

Basic

IsDiscreteValuationRing

ValuativeRel

Basic

Basic

ExtendToLocalization

Integers

Integral

IsTrivialOn

LocalSubring

PrimeMultiplicity

ValuationRing

ValuationSubring

AdjoinRoot

AlgebraTower

Bezout

ChainOfDivisors

EssentialFiniteness

EuclideanDomain

Filtration

FiniteLength

FinitePresentation

FiniteStability

FiniteType

FreeCommRing

FreeRing

HopkinsLevitzki

Idempotents

IntegralDomain

IsPrimary

IsTensorProduct

Length

MatrixAlgebra

MatrixPolynomialAlgebra

Multiplicity

Nakayama

OrzechProperty

PolynomialAlgebra

PowerBasis

PrincipalIdealDomain

PrincipalIdealDomainOfPrime

QuotSMulTop

ReesAlgebra

RingHomProperties

Support

SurjectiveOnStalks

SetTheory

Cardinal

Cofinality

Basic

Enum

Ordinal

Aleph

Arithmetic

Basic

Continuum

Defs

ENNReal

ENat

Finite

Finsupp

HasCardinalLT

NatCard

Order

Ordinal

Pigeonhole

Rat

Regular

SchroederBernstein

Subfield

ToNat

Ordinal

Arithmetic

Basic

Enum

Exponential

Family

FixedPoint

FundamentalSequence

Principal

Univ

Tactic (file)

Algebra

AlgebraNF

Basic

Lemmas

ArithMult (file)

Init

Attr

Core

Register

Bound (file)

Attribute

Init

CancelDenoms (file)

Core

CategoryTheory

Bicategory

Basic

Datatypes

Normalize

PureCoherence

Coherence (file)

Basic

Datatypes

Normalize

PureCoherence

Monoidal

Basic

Datatypes

Normalize

PureCoherence

BicategoricalComp

BicategoryCoherence

CancelIso

CategoryStar

CheckCompositions

Elementwise

IsoReassoc

MonoidalComp

Reassoc

Slice

ToApp

ClickSuggestions (file)

Apply

ApplyAt

FindPremises

GRewrite

Rewrite

SectionState

TryPremises

Unfold

Util

ComputeAsymptotics

Multiseries

Monomial

Basic

Predicates

Basic

Basis

Corecursion

Defs

Majorized

Trimming

Lemmas

Continuity (file)

Init

Determinant

Bird (file)

Cert

Meta

Explode (file)

Datatypes

Pretty

FieldSimp (file)

Attr

Discharger

Lemmas

Finiteness (file)

Attr

FunProp (file)

Attr

Core

Decl

Elab

FunctionData

Mor

Theorems

ToBatteries

Types

GCongr (file)

Core

CoreAttrs

ForwardAttr

GRewrite (file)

Core

Elab

Linarith (file)

Oracle

SimplexAlgorithm (file)

Datatypes

Gauss

PositiveVector

SimplexAlgorithm

FourierMotzkin

Datatypes

Frontend

Lemmas

NNRealPreprocessor

Parsing

Preprocessing

Verification

LinearCombination (file)

Lemmas

Linter (file)

TextBased (file)

UnicodeLinter

AuxLemma

CommandRanges

CommandStart

DeprecatedModule

DeprecatedSyntaxLinter

DirectoryDependency

DocPrime

DocString

EmptyLine

FindDeprecations

FlexibleLinter

GlobalAttributeIn

HashCommandLinter

HaveLetLinter

Header

Lint

MinImports

Multigoal

OldObtain

OverlappingInstances

PPRoundtrip

PrivateModule

Style

TacticDocumentation

UnusedInstancesInType

UnusedTactic

UnusedTacticExtension

UpstreamableDecl

ValidatePRTitle

Whitespace

Measurability (file)

Init

Monotonicity (file)

Attr

Basic

Lemmas

Nontriviality (file)

Core

NormNum (file)

Abs

Basic

BigOperators

Core

DivMod

Eq

GCD

Ineq

Inv

Irrational

IsCoprime

IsSquare

LegendreSymbol

ModEq

NatFactorial

NatFib

NatLog

NatSqrt

OfScientific

Ordinal

Parity

Pow

PowMod

Prime

RealSqrt

Result

Order (file)

Graph

Basic

Tarjan

CollectFacts

Preprocessing

ToInt

Polynomial

Basic

Core

Positivity (file)

Basic

Core

Finset

Push (file)

Attr

ReduceModChar (file)

Ext

Relation

Rfl

Symm

Ring (file)

Basic

Common

Compare

NamePolyVars

NamePowerVars

PNat

RingNF

Sat

FromLRAT

Simproc

Divisors

ExistsAndEq

Factors

FinsetInterval

VecPerm

Simps

Basic

NotationClass

TacticAnalysis (file)

Declarations

Translate

Attributes

Core

GuessName

Reorder

TagUnfoldBoundary

ToAdditive

ToDual

UnfoldBoundary

Widget

Calc

CommDiag

CongrM

Conv

GCongr

LibraryRewrite

SelectInsertParamsClass

SelectPanelUtils

StringDiagram

Abel

AdaptationNote

Algebraize

ApplyAt

ApplyCongr

ApplyFun

ApplyWith

BDSimp

Basic

ByCases

ByContra

Cases

CasesM

Change

Check

Choose

Clean

ClearExcept

ClearExclamation

Clear_

Coe

Common

ComputeDegree

CongrExclamation

CongrM

Constructor

ContinuousFunctionalCalculus

Contrapose

Conv

Convert

Core

CrossRefAttribute

DSimpPercent

DeclarationNames

DefEqAbuse

DefEqTransformations

DepRewrite

DeprecateTo

DeriveCountable

DeriveEncodable

DeriveFintype

DeriveTraversable

DuplicateDecls

ENatToNat

Eqns

ErwQuestion

Eval

ExistsI

Ext

ExtendDoc

ExtractGoal

FBinop

FailIfNoProgress

FastInstance

Field

FinCases

Find

FindSyntax

Generalize

GrindAttrs

Group

GuardGoalNums

GuardHypNums

Have

HaveI

HigherOrder

Hint

ITauto

InferParam

Inhabit

IntervalCases

IrreducibleDef

Lemma

Lift

LinearCombinationPrime

MinImports

MkIffOfInductiveProp

ModCases

Module

MoveAdd

NoncommRing

NthRewrite

Observe

OfNat

PNatToNat

PPWithUniv

Peel

Polyrith

ProdAssoc

ProxyType

Qify

RSuffices

Recall

Recover

Rename

RenameBVar

Replace

RewriteSearch

Rify

Says

ScopedNS

Set

SetLike

SetNotationForOrder

SimpIntro

SimpRw

SplitIfs

Spread

StacksAttribute

Subsingleton

Substs

SuccessIfFailWithMsg

SudoSetOption

SuppressCompilation

SwapVar

TFAE

Tauto

TautoSet

TermCongr

ToAdditive

ToDual

ToExpr

ToFun

ToLevel

Trace

TryThis

TypeCheck

TypeStar

UnsetOption

Use

Variable

WLOG

WithoutCDot

Zify

Topology

Algebra

Algebra (file)

Equiv

Group

Basic

ClosedSubgroup

Compact

Defs

GroupTopology

Matrix

Pointwise

Quotient

Torsor

InfiniteSum

Basic

Constructions

Defs

ENNReal

Group

Module

NatInt

Order

Real

Ring

SummationFilter

IsUniformGroup

Basic

Constructions

Defs

Order

MetricSpace

Lipschitz

Module

Alternating

Basic

Topology

ContinuousLinearMap

Basic

Idempotent

PiProd

Quotient

Restrict

RestrictScalars

Multilinear

Basic

Bounded

Topology

Spaces

CharacterSpace

ContinuousLinearMap

UniformConvergenceCLM

WeakBilin

WeakDual

Basic

ClosedSubmodule

Complement

Determinant

Equiv

FiniteDimension

FiniteDimensionBilinear

LocallyConvex

ModuleTopology

PerfectPairing

PerfectSpace

Simple

Star

UniformConvergence

Monoid (file)

Defs

FunOnFinite

Nonarchimedean

Bases

Basic

Order

Archimedean

Field

Floor

Group

Ring

Basic

Ideal

Real

SeparationQuotient

Basic

FiniteDimensional

Section

Star (file)

Real

ValuativeRel

ValuativeTopology

Valued

ValuationTopology

ValuedField

WithVal

Affine

AffineSubspace

ConstMulAction

Constructions

ContinuousAffineEquiv

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

MulAction

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

StarSubalgebra

Support

UniformConvergence

UniformField

UniformFilterBasis

UniformMulAction

UniformRing

WithZeroTopology

Baire

CompleteMetrizable

Lemmas

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Real

Category

TopCat

Limits

Basic

Products

Pullbacks

Adjunctions

Basic

EffectiveEpi

EpiMono

GrothendieckTopology

OpenNhds

Opens

ULift

TopCommRingCat

Compactness

Bases

Compact

CompactlyCoherentSpace

Lindelof

LocallyCompact

LocallyFinite

NhdsKer

SigmaCompact

Connected

Basic

Clopen

LocallyConnected

LocallyPathConnected

PathConnected

TotallyDisconnected

Constructions (file)

SumProd

ContinuousMap

Bounded

Basic

Normed

Star

Algebra

Basic

CocompactMap

Compact

ContinuousMapZero

ContinuousSqrt

Defs

Ideals

Lattice

Ordered

Polynomial

Star

StarOrdered

StoneWeierstrass

Units

Weierstrass

ZeroAtInfty

Covering

AddCircle

Basic

Quotient

Defs

Basic

Filter

Induced

Sequences

Ultrafilter

EMetricSpace

Basic

Defs

Diam

Lipschitz

Pi

FiberBundle

Basic

IsHomeomorphicTrivialBundle

Trivialization

GDelta

Basic

MetrizableSpace

Hom

ContinuousEval

ContinuousEvalConst

Homeomorph

Defs

Lemmas

Quotient

Homotopy

Basic

Contractible

Equiv

Path

Product

Instances

AddCircle

Defs

Real

ENNReal

Lemmas

EReal

Lemmas

NNReal

Lemmas

Real

Lemmas

Discrete

Int

Matrix

Nat

Rat

RealVectorSpace

Sign

ZMultiples

LocallyConstant

Basic

Maps

Proper

Basic

CompactlyGenerated

Strict

Basic

Basic

OpenQuotient

MetricSpace

ProperSpace (file)

Real

Pseudo

Basic

Constructions

Defs

Lemmas

Pi

Real

Algebra

Antilipschitz

Basic

Bounded

CantorScheme

CauSeqFilter

Cauchy

Completion

Contracting

Defs

Dilation

DilationEquiv

Equicontinuity

Gluing

HausdorffDistance

IsometricSMul

Isometry

Lipschitz

Perfect

PiNat

Polish

ThickenedIndicator

Thickening

UniformConvergence

Metrizable

Basic

CompletelyMetrizable

Real

Uniformity

OpenPartialHomeomorph

Basic

Composition

Constructions

Continuity

Defs

IsImage

Order (file)

AtTopBotIxx

Basic

Bornology

Compact

DenselyOrdered

ExtendFrom

IntermediateValue

IsLUB

Lattice

LeftRight

LeftRightLim

LeftRightNhds

LiminfLimsup

LocalExtr

Monotone

MonotoneContinuity

MonotoneConvergence

OrderClosed

ProjIcc

Real

Rolle

T5

PartialHomeomorph

Defs

Semicontinuity

Basic

Defs

Hemicontinuity

Separation

Basic

CountableSeparatingOn

GDelta

Hausdorff

Regular

SeparatedNhds

Sets

Closeds

CompactOpenCovered

Compacts

OpenCover

Opens

Sheaves

SheafCondition

OpensLeCover

PairwiseIntersections

Sites

UniqueGluing

Abelian

AddCommGrpCat

CommRingCat

Flasque

Forget

Functors

Init

Limits

LocalPredicate

LocallySurjective

MayerVietoris

Module

Over

PUnit

Presheaf

PresheafOfFunctions

Sheaf

SheafOfFunctions

Sheafify

Skyscraper

Stalks

Spectral

Basic

Hom

Prespectral

UniformSpace

AbstractCompletion

Basic

Cauchy

Compact

CompactConvergence

CompleteSeparated

Completion

Defs

DiscreteUniformity

Equicontinuity

Equiv

HeineCantor

LocallyUniformConvergence

Matrix

OfFun

Pi

Real

Separation

UniformApproximation

UniformConvergence

UniformConvergenceTopology

UniformEmbedding

AlexandrovDiscrete

Bases

Basic

Clopen

Closure

ClusterPt

Coherent

CompactOpen

Constructible

Continuous

ContinuousOn

DenseEmbedding

DiscreteSubset

ExtendFrom

Gluing

IndicatorConstPointwise

Inseparable

Irreducible

IsLocalHomeomorph

JacobsonSpace

KrullDimension

LocalAtTarget

LocallyClosed

LocallyFinite

Neighborhoods

NhdsKer

NhdsSet

NhdsWithin

NoetherianSpace

Path

Perfect

Piecewise

QuasiSeparated

SeparatedMap

Sequences

Sober

Ultrafilter

UnitInterval

UrysohnsLemma

WithTopology

Util

AtomM (file)

Recurse

AddRelatedDecl

AtLocation

CompileInductive

CountHeartbeats

DelabNonCanonical

Delaborators

DischargerAsTactic

ElabWithoutMVars

Notation3

PPOptions

ParseCommand

PrintSorries

Qq

Superscript

SynthesizeUsing

Tactic

TermReduce

TransImports

WhatsNew

WithWeakNamespace

Init

Plausible (file)

Arbitrary

ArbitraryFueled

Attr

DeriveArbitrary

DeriveShrinkable

Functions

Gen

Random

Sampleable

Shrinkable

Tactic

Testable

ProofWidgets

Component

Panel

Basic

Basic

FilterDetails

HtmlDisplay

MakeEditLink

OfRpcMethod

PenroseDiagram

RefreshComponent

Data

Html

Presentation

Expr

Cancellable

Compat

Util

Qq (file)

ForLean

Do

ReduceEval

ToExpr

AssertInstancesCommute

Commands

Delab

Macro

Match

MatchImpl

MetaM

Simp

SortLocalDecls

Typ

Std (file)

Async (file)

Basic

ContextAsync

DNS

IO

Process

Select

Signal

System

TCP

Timer

UDP

Data (file)

DHashMap (file)

Internal

AssocList

Basic

Iterator

Lemmas

Defs

HashesTo

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawDef

RawLemmas

DTreeMap (file)

Internal

WF

Defs

Lemmas

Balanced

Balancing

Cell

Def

Lemmas

Model

Operations

Ordered

Queries

Zipper

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ExtDHashMap (file)

Basic

Lemmas

ExtDTreeMap (file)

Basic

Lemmas

ExtHashMap (file)

Basic

Lemmas

ExtHashSet (file)

Basic

Lemmas

ExtTreeMap (file)

Basic

Lemmas

ExtTreeSet (file)

Basic

Lemmas

HashMap (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

HashSet (file)

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

Internal

List

Associative

Defs

Cut

Iterators (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

StepSize

TakeWhile

Zip

Drop

DropWhile

StepSize

TakeWhile

Zip

Consumers (file)

Monadic (file)

Set

Set

Lemmas (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

FilterMap

TakeWhile

Zip

Drop

DropWhile

TakeWhile

Zip

Consumers (file)

Monadic (file)

Collect

Loop

Set

Collect

Loop

Set

Equivalence (file)

Basic

HetT

StepCongr

Producers (file)

Monadic (file)

Array

Empty

List

Vector

Array

Empty

Range

Repeat

Slice

Vector

Monadic

Producers (file)

Monadic (file)

Array

Empty

Vector

Array

Empty

Range

Repeat

Slice

Vector

String (file)

ToInt

ToNat

TreeMap (file)

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

TreeSet (file)

Raw (file)

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ByteSlice

Do (file)

Internal (file)

Ensures (file)

Def

Lemmas

SPred (file)

Notation (file)

Basic

DerivedLaws

Laws

SPred

SVal

Triple (file)

Basic

SpecLemmas

WP (file)

Basic

Monad

SimpLemmas

Sound

PostCond

PredTrans

Http (file)

Data (file)

Body (file)

Any

Basic

Empty

Full

Length

Stream

Headers (file)

Basic

Name

Value

URI (file)

Basic

Config

Encoding

Parser

Chunk

Extensions

Method

Request

Response

Status

Version

Internal (file)

Char

ChunkedBuffer

Encode

IndexMultiMap

LowerCase

String

Protocol

H1 (file)

Config

Error

Event

Message

Parser

Reader

Writer

Server (file)

Config

Connection

Handler

Test

Helpers

Transport

Internal (file)

Do (file)

Order

Basic

Frame

Lemmas

Triple (file)

Basic

Gadget

SpecLemmas

WP (file)

Basic

Lemmas

Assertion

ExceptPost

PredTrans

Parsec (file)

Basic

ByteArray

String

UV (file)

DNS

Loop

Signal

System

TCP

Timer

UDP

Net (file)

Addr

Sat (file)

AIG (file)

RefVecOperator (file)

Fold

Map

Zip

Basic

CNF

Cached

CachedGates

CachedGatesLemmas

CachedLemmas

If

LawfulOperator

LawfulVecOperator

Lemmas

RefVec

Relabel

RelabelNat

CNF (file)

Basic

Dimacs

Literal

Relabel

RelabelFin

Sync (file)

Barrier

Basic

Broadcast

CancellationContext

CancellationToken

Channel

Mutex

Notify

RecursiveMutex

Semaphore

SharedMutex

StreamMap

Tactic (file)

BVDecide (file)

Bitblast (file)

BVExpr (file)

Circuit (file)

Impl (file)

Operations

Add

Append

Clz

Cpop

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

Reverse

RotateLeft

RotateRight

ShiftLeft

ShiftRight

Sub

Udiv

Ult

Umod

ZeroExtend

Carry

Const

Expr

Pred

Substructure

Var

Lemmas (file)

Operations

Add

Append

Clz

Cpop

Eq

Extract

GetLsbD

Mul

Neg

Not

Replicate

Reverse

RotateLeft

RotateRight

ShiftLeft

ShiftRight

Sub

Udiv

Ult

Umod

ZeroExtend

Basic

Carry

Const

Expr

Pred

Var

Basic

BoolExpr (file)

Basic

LRAT (file)

Internal

Formula (file)

Class

Implementation

Instance

Lemmas

RatAddResult

RatAddSound

RupAddResult

RupAddSound

Actions

Assignment

CNF

Clause

CompactLRATChecker

CompactLRATCheckerSound

Convert

Entails

LRATChecker

LRATCheckerSound

PosFin

Actions

Checker

Parser

Normalize (file)

BitVec

Bool

Canonicalize

Equal

Prop

Reflect

Syntax

Do (file)

ProofMode

Syntax

Time (file)

Date (file)

Unit

Basic

Day

Month

Week

Weekday

Year

Basic

PlainDate

ValidDate

DateTime (file)

PlainDateTime

Timestamp

WallTime

Format (file)

Basic

DateFormat

Internal (file)

Bounded

UnitVal

Notation (file)

Spec

Time (file)

Unit

Basic

Hour

Millisecond

Minute

Nanosecond

Second

Basic

HourMarker

PlainTime

Zoned (file)

Database (file)

Basic

TZdb

TzIf

Windows

TimeZone

ZoneRules

Duration

Color scheme

darksystemlight