General documentation

index

foundational types

tactics

references

Library

Aesop (file)

Builder

Apply

Basic

Cases

Constructors

Default

Forward

NormSimp

Tactic

Unfold

BuiltinRules (file)

ApplyHyps

Assumption

DestructProducts

Ext

Intros

Rfl

Split

Subst

Forward

Match (file)

Types

State (file)

ApplyGoalDiff

Initial

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

Lemmas

Data

Array

Basic

Lemmas

Merge

Scan

BinomialHeap

Basic

Fin

Basic

Lemmas

List

Basic

Count

Lemmas

Pairwise

Perm

MLList

Basic

Nat

Bitwise (file)

Lemmas

Basic

Lemmas

Vector

Basic

Lemmas

Except

UInt

Lean

Meta

Basic

DiscrTree

Expr

Inaccessible

InstantiateMVars

SavedState

UnusedNames

AttributeExtra

Except

Expr

HashSet

MonadBacktrack

NameMapAttribute

PersistentHashMap

PersistentHashSet

Position

Syntax

TagAttribute

Linter (file)

UnnecessarySeqFocus

UnreachableTactic

Tactic

Lint (file)

Basic

Frontend

Misc

Simp

TypeClass

Alias

Basic

Case

Congr

Exact

GeneralizeProofs

HelpCmd

Init

PermuteGoals

SeqFocus

Trans

Unreachable

Util

Cache

ExtendedBinder

LibraryNote

ProofWanted

Logic

Complexity (file)

Algorithms

Lean

FusionTree

Capacity

Compression

Correction

Multiplier

Routing

Sketch

Tree

XorCorrection

SearchTree

Basic

Cost

Erase

Stateful

Sort

Bitonic

Basic

Correctness

Trace

ZeroOne

VanEmdeBoas

Basic

Elements

Insert

Layout

Successor

Queue

Retroactive

Reachability

InductiveCounting (file)

Bounds

Completeness

Progress

Semantics

BreadthFirst

Reingold

ReingoldEval

Savitch

WordRAM

FusionTree

Node (file)

Correction

Header

Initial

Neighbors

Registers

Semantics

Sketch

Query (file)

Node

Program

Traversal

Binary

Boundary

Compress

LowerRank

MSB

MSBProgram

Model

Neighbors

Packed

Parameters

Preprocessing

Rank

ReadHeader

Static

PrefixSums

Dynamic

Query

Tree

Update

Queue

Basic

Dynamic

Model

Stack (file)

Controller

VanEmdeBoas

Init (file)

Table

Call

Insert

Member

Model

Program

Successor

DynamicArray

ElementDistinctness

ElementDistinctnessRAM

Computability

BitString

Padding

BranchingProgram

MonoidProgram

PolyLength

Circuit

Approximation (file)

Hamming

Arithmetic (file)

Hessian (file)

SourceComplexity

Waring (file)

Basic

Compilation

Determinant

Formula

Pairing

Power

VNP

VP

Boolean

ACC0 (file)

Basic

Simulation

AffineDisperser (file)

Deletion

Elimination

MinimalAnd

Normal

Operations

Reduction

Reparameterisation

Rewiring

State

Step

AltFormula (file)

TopDown

CarryLookahead (file)

PolyTime

CarrySave (file)

Reduce (file)

PolyTime

PolyTime

DepthTime (file)

PolyTime

Encoding (file)

Certificate

FirstOrder (file)

Parity

Formula (file)

Andreev

Restriction

Subbotovskaya

HardnessAmplification (file)

Schedule

Stages

WorstCase

Hastad (file)

Sharp

Iteration (file)

CounterChart

Basic

Circuit

Decode

Encode

Time

ModulusCounter (file)

Basic

Remainders

Active

AffineController

Batch

CircuitCounting

CounterBatch

Decoder

Depth

DepthSearch

Encoded

Eventual

ForestCircuitRecords

ForestCircuits

ForestQuerySynthesis

ForestRecordQueries

InPlace

InputTime

Label

LabelCircuit

LongTime

NavigationCircuits

NavigationFeatures

NavigationSynthesis

NavigationWord

Optimization

Permutation

PrimeCycles

Record

RecordCircuit

Remainder

Residue

ResidueAdd

Scan

Selection

SequentialSquaring

SharedDictionary

SparseDisplacement

SparseNavigation

SparseTime

Target

UniversalMap

VisitScheduleCircuits

Layered (file)

Compile (file)

Correctness

PolyTime

Size

Padding (file)

PolyTime

PolyTime

Size

MassProduction

Pipeline (file)

Circuit

Packing

Scheduler (file)

Basic

Cost

Phase

PhaseCircuit

State

Uhlig (file)

Layer

Basic

Fine

FineParameters

FineStatement

Padding

Schedule

Synthesis

Modular

InnerProduct (file)

PolyTime

Multiply (file)

PolyTime

PartialProduct (file)

PolyTime

Subtract (file)

PolyTime

NaturalProof (file)

Generator

SemiCircuit (file)

Equation

Gate

OfCircuit

Reparameterisation

Rewiring

Simplification

ShallowSymmetric (file)

Bounds

Construction

Covering

Moduli

ShiftTest

Weights

Smolensky (file)

Approximation

Gates

Majority

Tableau

Basic

Correct

Layout

Space

Threshold (file)

Parity

WeightedThreshold (file)

Activation

Activity

ActivityBounds

Capacity

CapacityCircuit

Components

Cut

InnerProduct

Menus

PendingBias

Potential

ScalarActivity

TranscriptTree

AC0

Advice

AtLeast

BalancedCode

Barrington

BarringtonClass

BatchLookup

BatchOr

BinaryCost

BitBlast

BoundedError

Broadcast

CodeComposition

CodeSubstitution

CodeTemplate

CompareSwap

Comparison

Conondeterministic

ConstDepth

Continuity

Correction

DepthClasses

DuplicateFlags

ElementDistinctness

EncodingSize

Equality

EvaluationTime

FanInTwo

GateElimination

Gates

Hamming

HardCore

Hierarchy

KarchmerWigderson

KeyedSort

Khrapchenko

KhrapchenkoDepth

LMN

MachineSimulation

Majority

Metric

Minterms

ModGates

ModMajority

Multiplicity

Nechiporuk

NegationNormalForm

NonconstantCost

Nondeterminism

Oracle

PPoly

PPolyHard

Parity

PolynomialTime

Propagation

Routing

RoutingValues

SeedFixing

ShannonConstruction

ShannonSynthesis

Sorting

SortingTrace

Sparse

SparseSynthesis

SparseSynthesisConstruction

Spira

Substitution

Synthesis

TC0

ThresholdNC1

TopDown

Tournament

Unbounded

Word

XorLemma

Yablonskii

Cyclic (file)

Feedback

Encoding

MapOp

Frontier

Compiler (file)

Network

Correlation (file)

Asymptotics

Circuit

Rectangle

Layouts

Gaussian (file)

Basic

Coefficient

EdgeScores

Sample

Straddle

Basic

BoundedDegree

Components

Compression

Core

Cubic

General

Kernel

Local

Median

MultiGaussian

MultiOrder

Scores

Support

VertexGaussian

Ledger

Aggregate

Basic

LowerBound

Sweep

Unconditional

Linear

LowerBound

Unconditional

AverageCase

BoundedFanIn

BranchingProgram

Demand

FanInTwo

LowerBound

Multigraph

Network

Nondeterministic

Projection

Rectangle

Reduction

Sweep

Unconditional

Witness

Fusion

Cyclic (file)

Closure

Compiler

Graph (file)

Canonical

Inequality

Random

Basic

Boolean

Certificate

CertificateCircuit

Composition

Conondeterministic

Consistency

Converse

Counting

DeMorgan

Encoding

Extension

Homomorphism

Pullback

Quadratic

Sampling

Semifilter

Simulation

SimulationContext

Monotone

Clique

Approximator

Asymptotic

Essential

LowerBound

Negative

Positive

Basic

BipartiteMatching

DualRail

Formula

KarchmerWigderson

Set

Rational (file)

MatrixEval (file)

Defs

Runtime (file)

Lift (file)

Defs

Determinant

Encode

Parameters

Point

Affine

BlockDivision

Certificates

CyclotomicGrid

Deformation

Defs

Determinant

EncodingBounds

Eval

Executable

Generator

IntegralLift

LaurentReduction

PaddedRank

QuantumMatrices

QuantumSeries

Rectangular

SmallExpansion

Wronskian

SumOfTerms (file)

Basic

Coverage

Balanced

Basic

BipartiteMatching

Bird

Clique

Complexity

CompositionDepth

Continuity

Decomposable

Depth

Erase

Evaluation

FanIn

Formula

FullArithmetic

HintDecoding

InnerSize

Iteration

KernelVector

Linearize

MapLines

MapOp

Metric

Parallel

Pi

Pointwise

Program

ReedMullerDecoding

Replication

SignatureHom

Simulation

SimulationContext

SimulationDepth

SourceComplexity

Support

Synthesis

Unfolding

Wiring

Communication

TopDown

Adversary

Majority

Parity

Rectangle

Amplification

Corruption

Discrepancy

Disjointness

Distributional

Equality

FoolingSet

Functions

Inclusion

InnerProductRank

KarchmerWigderson

Newman

Operations

Protocol

Randomized

Rank

Rectangle

RoundProtocol

Complexity

AffineDisperser (file)

BinaryPolynomial

Coordinates

PolyTime

Program

Classes

AWPP (file)

Amplification

Closure

Lowness

OracleWeights

WPP

Alternation (file)

Game

GuessVerify

NP

Savitch

TQBF

ArthurMerlin (file)

Amplification

Collapse

GraphNonIsomorphism

PH

SetLowerBound

BPP (file)

Derandomization (file)

Generator

Amplification

Collapse

KarpLipton

Reduction

WorstCaseHardness

BooleanHierarchy (file)

Closure

Kadin

PH

Counting

OracleSpace

Space

FewP (file)

Machine

Hierarchy (file)

ShortDesc

Space

Time

IP (file)

TQBF (file)

Protocol

Tokens

Verifier

Words

CoinFixing

GameTree

GraphNonIsomorphism

Guessing

OptimalProver

PSPACE

Reduction

Repetition

Shamir

Simulation

Ladner (file)

Basic

PolyTime

LogSpace (file)

FirstOrder (file)

Ordered (file)

Reduction

Formula

Output

Reduction

Transducer

Complement

PolyTime

USTCON

MIP (file)

Defs

NEXP

OptimalProver

ModP (file)

GapP

NP (file)

Closure

GuessVerify

Nondeterministic

SelfReduction

Witness

Oracle (file)

BakerGillSolovay

Closure

Collapse

Counting

CountingEquivalence

Deterministic

Diagonal

Lowness

Monotone

PP

PolyTime

Replay

Simulation

Space

TQBF

P (file)

Closure

Complement

Slices

PCP (file)

NP

ZeroRandomness

PH (file)

Closure

Collapse

Kannan

KarpLipton

Projection

SipserLautemann

PP (file)

Bit

Characterization

Closure

Oracle

TruthTable

ParityP (file)

Closure

Promise

Basic

Circuit

Reduction

RP (file)

Closure

SBP (file)

Amplification

SPP (file)

FewP

SharpP (file)

Aggregation

Characterization

Closure

Combinators

Completeness

GapMachine

Lowness

Machine

Oracle

PolyTime

Power

Probability

Products

Space

WeightedReplay

Space (file)

GeneralizedGeography (file)

Membership

Reduction

TQBF (file)

Evaluation

Formula

Membership

PolyTime

Prenex

Reduction

Basic

Closure

Savitch

TM2

Time

TFNP (file)

Subclasses (file)

Completeness

Principles

SearchToDecision

Toda (file)

Counting

Hierarchy

Isolation

UP (file)

Machine

ValiantVazirani (file)

Collapse

Reduction

WPP (file)

Bounded

Lowness

Robustness

TruthTable

TwoSided

CeqP

Constructible

DP

EXP

Inclusions

Operators

Padding

RepeatedTrials

Time

US

ZPP

CookLevin

Clauses

Completeness

Correctness

Counting

Encoding

Parameters

Parsimonious

PolyTime

Reduction

Tableau

Fagin

Tableau (file)

Defs

Semantics

Converse

Layout

Ordered

Power

SAT

Small

StrictVerifier

Verifier

FineGrained (file)

Assignment

BruteForce

Exponents

GraphProblems

OrthogonalVectors

Reduction

Sparsification

HardnessEncoding

PolyTime

Program

Parameterized (file)

VertexCover (file)

BussKernel

Kernelization

Problems

CircuitValue (file)

Compilation

Completeness

Writer

Hamiltonian (file)

Diamond (file)

Defs

Soundness

Directed

Sparse

Undirected

IndependentSet (file)

Sparse

MonotoneCircuitValue (file)

Completeness

SAT (file)

PolyTime

SubsetSum (file)

Digits

Mask

TQBF (file)

Closed

CircuitSAT

Clique

Coloring

CountingSAT

ExactThreeSAT

GeneralizedGeography

Graph

GraphIsomorphism

IntegerProgramming

Knapsack

Partition

SATUNSAT

SharpSAT

TSP

ThreeSAT

USAT

USTCON

VertexCover

Reduction (file)

ManyOne

TruthTable

ProofSystem

DecisionTree

AffineScore

Basic

CanonicalTree

Certificate

Fourier

Granularity

Influence

InnerProduct

Leaves

NormalForm

Observations

Parity

Restrict

Sensitivity

Separable

SpectralNorm

Switching

Symmetric

GenericRAM

Native (file)

Combinators

Nat

Simulation

Finite

Run

Turing

SparseMemory

Basic

Turing

Algebraic

Defs

Signed

Interactive

Basic

Plain

Security

Sequential

Sumcheck

Kolmogorov

Basic

ChainRule

Depth

Incompressibility

Invariance

MultiTape

NisanWigderson

Partrec

SelfDelimiting

SingleTape

Uncomputability

Languages

Slice

MCSP

AntiChecker

Basic

NP

Shannon

Succinct

Machines

ReadMachine

Basic

StepMachine

Tidy

Turing

MultiTape

Combinators

Append

Comp

CopyWord

Encoding

Foldl

Id

Ite

IterateWhile

MultiPass

Reverse

StepMachine

StreamFold

TidyNormalForm

TidyZeroSpace

Transducer

Complexity

BigO (file)

Constructible

Option

Pi

Plain

Sum

InSpace (file)

Bit

Plain

LogSpace (file)

ConfigurationGraph (file)

Basic

Bounds

Correctness

Radix

Routines

Tape

CounterProgram (file)

Output

InductiveCounting (file)

Bounds

Callbacks

Encoding

Graph

Machine

Routines

NondeterministicQueryMachine (file)

Bounds

Compiler

Native

Routines

Termination

Configurations

QueryMachine

Reachability

PolySpace (file)

Fold

Plain

PolyTime (file)

Int (file)

Binary

BinaryDiv

Matrix

Binary

Nat (file)

Binary

BinaryDiv

Div

Factorial

Fin

Gcd

Log

PowMod

Prime

Search

RotationMap (file)

TowerTable (file)

Family

Family

Tower

Walk

Basic

BitString

Configuration

DPi

Finite

Fold

Iteration

Length

List

Membership

Option

Pi

Plain

Sum

Tape

Window

Space (file)

Decode

Reachability

Savitch

Arith

BigOLe

Binary

BinaryCompare

Degree

Fold

InSpaceLib

LinearSpaceArith

Lists

Nondeterministic

Primitives

Quantitative

SpaceInTime

Streaming

Translate

Counting (file)

Oracle

Program

Replay

Alternative

Binary

Certificate

Checker

Composition

Deterministic

Execution

ExtendTapes

Guess

OutputPrefix

Program

Sequential

Verdict

Verifier

Encodings

IntBinary (file)

Decode

Basic

Configuration

DPi

Decoder

Finite

Frame

Length

List

MultiPass

Nat

NatLength

NatPower

NatStream

Option

Pair

Pi

StepMachine

StepMachineComp

StreamFold

Sum

Tape

Halting (file)

Basic

Computable

Hardwire

Partialize

Partrec

Reduction

Rice

SMN

Machine (file)

ChoiceTable

Clock

Composition

Equivalence

ExtendTapes

Finite

Halting

InputFromTape

Nondeterministic

OutputPrefix

OutputToTape

Program

Sequential

Simulation

Space

Plumbing

Tidy

Basic

Defs

Run

Branch

ClearShadowed

Cursor

ExtendTapes

ExtendTapesView

InputFromTape

InputHead

MarkWork

OnWords

OutputToTape

PrepareClock

PrepareInput

PreparePair

ReadInput

RepeatUntilBlank

RewindWork

Sequential

Shadow

TransformsTapes

TransformsWords

WhileCond

WhileInput

Probabilistic (file)

Tidy (file)

Redirect

Clock

Closed

CoinTape

Composition

Deterministic

ExtendTapes

InputFromTape

IterateWhile

Loop

Oracle

OutputPrefix

OutputToTape

PolynomialClock

QueryBounds

QueryTake

Replay

ReplayInput

RunsWords

Sampling

Sequential

SingleOracle

StepMachine

Basic

Comp

Universal

Basic

Bound

Complexity

Compose

Correct

Decode

InPlace

Machine

PolyTime

ResourceBound

Space

SpaceBudget

Configuration

Deterministic

Feature

FiniteConfiguration

Map

Nondeterministic

OutView

PolyTime

ResourceBounds

Run

SingleTape

Space

TapeLemmas

SingleTape

Partrec

PostTuringMachine

TM2

ConfigBound

Encoding

PolySpace

PolyTime

Simulation

PCP

Amplification (file)

Arithmetic

Family

Approximation

Hastad (file)

LinearTest

IndependentSet

LabelCover

MaxCSP

MaxExactThreeSAT

MaxThreeSAT

AssignmentTester (file)

Selection

Encoded

Amplification (file)

Arithmetic

Enumeration

Iteration

AssignmentTester (file)

Enumeration

Composition (file)

Enumeration

GenericComposition (file)

Enumeration

Preprocess (file)

Programs

SelectedComposition (file)

Enumeration

Verifier (file)

Reduction

Repetition

Soundness

AddTrivial

Basic

Cloud

CloudRotation

Constraints

DegreeReduction

GapTheorem

Iteration

Power

SelectedAssignmentTester

Size

ThreeSAT

Power (file)

Complexity

WithInput

Amplifier

Completeness

Composition

ConstraintGraph

DegreeReduction

GapTheorem

GenericComposition

LocalTest

PoweringBound

Preprocess

RegularConstraintGraph

SelectedComposition

ThreeSAT

Probabilistic

Oracle (file)

Composition

Iteration

Memoize

Normalization

Parameter

SingleOracle

Substitution

Tidy

PPT (file)

Capture

Clock

Composition

Realization

OpenOracleSimulation

OracleSimulation

Adaptive

BoundedUniform

CenteredBinomial

CoinTape

Finite

LinearHash

Memoize

OracleSimulation

Parameter

Presample

QueryBounds

Repeat

Sampling

Selection

Traverse

UniformNat

QueryComplexity

ApproximateDegree (file)

Or

Randomized (file)

Nisan

SensitivitySeparation (file)

Internal

Basic

Bridge

Composition

ConstructedSeed

Construction

Defs

FixedCoordinates

HammingBase

InitialPredicates

Iterates

Labeling

LabelingBounds

LabelingConstraints

LabelingEstimate

LabelingEvents

Or

ParameterBounds

PowerAmplification

ProfileArithmetic

QuantitativeProfiles

Recursive

RecursiveBlocks

RecursiveCandidates

RecursiveChildren

RecursiveDefinitions

RecursiveFailures

RecursiveFlips

RecursiveJointZero

RecursiveOne

RecursiveProfiles

RecursiveRepair

RecursiveSets

RecursiveZero

Reindex

ScalarBounds

SeedAmplification

Separation

SeparationArithmetic

Tournament

TournamentCounts

TournamentCyclic

Tower

TowerProfiles

Degree

Huang

Monotone

NisanSzegedy

OneSided

Relations

Restriction

SensitivityBounds

Threshold

Yao

RAM

Cost

Defs

Input

Squaring

Reduction

ManyOne

TreeEval

Ary

Basic

CookMertz

Reader

Cert

Machine

Offset

Regs

Residue

Step

Weight

Arith

Correct

Defs

Encode

Invariant

Size

Tuple

Basic

CookMertz

Encoding

Instance

Iterative

Space

USTCON

Reader

Cert

Correct

Defs

Encode

Invariant

Space

WordRAM

Multiword (file)

Arithmetic

Bank

BankArithmetic

BankOps

BankScalar

Bitwise

Circuit

CircuitRun

Compile

Digits

Mul

Shift

Sub

Transfer

Workspace

Allocation

Basis

Compile

Controller

Copy

Defs

Dynamic

Function

Generic

Heap

MapOp

Native

Notation

PackedCount

RAM

RAMInput

Structured

Time

Trace

Crypto

Computational

DiscreteLog (file)

SchnorrGroup

Encryption

Basic

Circular

PolyTime

PublicKeyReplacement

GGM

Circuit

Evaluation

Expansion

Hybrid

Reduction

Security

GMW

PolyTime

Protocol

Simulator

Soundness

GoldreichLevin

Decoding

HardCore

Nonuniform

Parameters

Reduction

WordDecoder

WordReduction

Homomorphic

BitEncryption (file)

PolyTime

Circuit (file)

PolyTime

Evaluation (file)

PolyTime

FixedKey

Basic

Bootstrapping

Correctness

Encoding

PolyTime

Reduction

Security

GSW

DecryptionCircuit (file)

Parameters

PolyTime

DepthParameters (file)

Security

Sampling (file)

Randomness

Serialized

Serialized (file)

Evaluation (file)

PolyTime

Correctness

PolyTime

Basic

Decoding

Decryption

Gadget

Hiding

LWE

Noise

Parameters

Security

KeyChain (file)

Hybrid (file)

Game

PolyTime

Reduction (file)

Game

PolyTime

PolyTime

Security

Layered (file)

Correctness

PolyTime

Leveled

Reduction (file)

Game

PolyTime

Basic

Bootstrapping

Compactness

Correctness

Encoding

PolyTime

Security

Basic

Efficiency

Refresh

Hybrid

SavedPrediction

Sequence

LWE

Basic

OneWay (file)

BPP

Collision

MCSP

NP

Normalize

Pseudoentropy

Boosting

Clipped

Decision

Learner

Loop

Potential

Program

Progress

Sampling

Selection

Training

ThreeSource (file)

Amplification

Candidates

Combined

Padding

Seeded

Basic

DenseMask

EntropyGrid

ExtractionSchedule

Generator

HashPair

HashReduction

LabelExtraction

Learning

MaskedExtraction

Masking

MatrixExtraction

OneWay

Reduction

RepeatedExtraction

Seed

SeedExtraction

Selection

SequenceLearner

WordExtraction

WordReduction

WordSeedExtraction

PseudorandomFunction (file)

RandomOracle

TruthTable

Stretch (file)

Quantitative

Basic

CollisionResistant

Commitment

GeneratorPadding

GeneratorReindex

GeneratorXor

HardCore

MAC

MerkleDamgard

OneWayToPRF

OneWayToPRG

OneWayToSignature

PRGToOneWay

Prediction

PseudorandomGenerator

SchnorrIdentification

Signature

UniformChoice

ZeroKnowledge

Game (file)

Hybrid

Statistical

UntilBad

Negligible (file)

Basic

Dyadic

Primitives

PRG

NisanWigderson (file)

Circuit

Derandomization

Design

Reconstruction

Sampling

Circuit

Game

NextBit

Protocols

Cipher

EvenMansour

SigmaProtocol

Basic

Composition

FiatShamir

Identification

Linear

SchnorrIdentification

SchnorrSignature

Signature

RandomOracle

Foundations

Analysis

SpecialFunctions

Arccos

BernoulliInequality

HarmonicMean

MarkovInequality

BooleanAnalysis

Hypercontractivity (file)

Derivative

LpNorm

Tensorization

TwoPoint

Bernoulli

Bonami

BucketWeight

Convolution

CoordinateSampling

Decomposition

Degree

Fibers

Fourier

FourierDegree

FourierRestriction

FriedgutJunta

Hadamard

HadamardRectangles

HadamardTester

HammingFourier

HarmonicMean

Hypercube

Influence

KahnKalaiLinial

LightPatterns

Linearity

LongCode

LowDegree

LowDegreeParity

MirrorSets

Monotone

MultilinearExtension

Noise

PolynomialCorrelation

RelevantCoordinates

SignApproximation

Symmetrization

Combinatorics

AffineDisperser (file)

AffineSubspace

BinaryField

Bits

Explicit

IndependentSources

Threshold

Expander

Walk (file)

WithInput

AffineFamily

AffinePlane

AffineTower

Basic

Cheeger

Connected

Contraction

Existence

Family

Hitting

Hom

KilledWalk

Lazy

Loops

LowerBound

Mixing

Multigraph

Perm

Power

Products

Random

Reindex

Reingold

ReingoldVertex

SimpleGraph

SlotGraph

Tower

TowerBase

TowerFamily

FiniteCover (file)

Basic

FunctionalGraph (file)

Active

CheckpointForest

Checkpoints

Commutation

Cycle

DistinguishedPoints

ForestDuality

ForestIntervals

ForestNavigation

ForestSegments

HittingTime

Powers

Projection

Spectrum

LineCode

HighRate (file)

Monomial

Packing

Rate

Systematic

Menu (file)

Collision

Counting

Basic

Line

SimpleGraph

Metric

Sunflower (file)

LowerBound

Pluck

CentralBinomial

DepthReduction

Hypergeometric

Lautemann

MajorityVote

Multigraph

PowersetTail

Control

Monad

IsMonadHom

StateT

Memoize

Data

BitString

List (file)

Binary

Operations

Vote

Parity (file)

Weight

PartialAssignment (file)

Counting

AffineDisperser

Agree

Basic

Binary

Block

Broadcast

Counter

CoverCoding

Enumeration

Flip

Hamming

HighestDiff

Hoeffding

Multiplication

PackedCount

Packing

Point

Projection

Propagation

QuadraticForm

Selection

ShortWords

Sign

Sparse

SumTree

Uhlig

Weight

WordCount

ZModTwo

Code

Basic

BerlekampWelch

Concatenation

Hadamard

HammingBound

HintDecoding

Johnson

Justesen

Linear

LocalDecoding

LocalListDecoding

LowDegreeExtension

ReedMuller

ReedSolomon

SelfCorrection

Singleton

Sudan

SudanInterpolant

Fin

Append

Order

Tuple

Finset

Expect

Quantile

Sampling

SymmDiff

List

Append

BalancedFold

Basic

Counting

Equiv

Fold

Lookup

OfFn

Matrix

Binary

Permanent

TotallyRegular

MvPolynomial

Catalecticant

DualNumber

Hessian

HessianRank

Nat

Choose (file)

Real

PolynomialBound

Closure

Exponential

Log

Bits

Card

Div

IntermediateValue

Log

Prime

Primrec

Radix

OrderedSet (file)

Spec

Polynomial

CoeffList

SignQueries

Seq

Computation

Set

Card

BiTape

Hamming

HammingBound

ListDecoding

StackTape

FieldTheory

Finite

BinaryField

LinearizedPolynomial

ReducedMonomial

Subfield

UnitSum

TensorBasis

Geometry

Euclidean

Angle

Cap

GroupTheory

Perm

Fin

FiveCycle

Last

LinearAlgebra

Matrix

CutRank

Lindsey

Moore

Rank

SubmatrixRobust

Toeplitz

CubeSum

Interpolation

KernelVector

PivotSpace

Rank

Order

Changes

UpperLower

Probability

Gaussian

Multivariate

Real

Sheppard

SecondMoment

Relation

InductiveCounting

RelatesWithinSteps

Semantics

Stateful

Amortized

Basic

Composition

CostHoare

Hoare

Module

Realization

Resource

Languages

Probabilistic

Oracle (file)

Interaction

QueryCount

Simulation

Support

Transcript

RandomOracle (file)

Probabilistic

Basic

BitString

BoundedUniform

CenteredBinomial

Concentration

Forking

Iteration

LinearHash

Memoize

Notation

Presample

QueryCount

Repeat

Selection

Simulation

Sum

Transcript

Traverse

UniformNat

UntilBad

Vector

Logics

FirstOrder

Encoding (file)

Layout

Interpretation (file)

Constants

Encoding

Rank

Tagged

Tuple

Unit

Ordered

BitSum (file)

Encoding

DomainInterpretation (file)

Certificate

Composition

Encoding

FullTuple (file)

Composition

DomainInterpretation

Encoding

Multiplication (file)

Blocks

Bounds

Columns

Radix

Arithmetic

Bit

Conversion

Decode

Multiplication

Tuple (file)

Flatten

Addition

Basic

BitArithmetic

Constants

Interpretation

Packing

Query

Reduction

TupleBit

TupleInterpretation

TupleSuccessor

Problems

CNF

Coloring

ColoringReduction

ColoringToCNF

IndependentSetReduction

SizedGraph

Projection (file)

Graph

Reduction (file)

Nontrivial

QuantifierFree

Basic

ProjectionFormula

QuantifierFree

Subformula

Tuple

Propositional

CNF (file)

ThreeCNF (file)

PolyTime

Coding

Compact

ExactlyOne

ModelCount

Parity

PolyTime

UnsatVal

ClauseSet

Sparsification (file)

Bounds

List

Path

PolyTime

Search

Step

Tree

Basic

SubcubeFree

Parity (file)

DepthThree

QBF (file)

Arithmetization

Resolution (file)

Pigeonhole

Proof

SizeWidth

TreeLike

Tseitin

TseitinExpander

DNF

Pigeonhole

SigmaThree

Tseitin

SecondOrder

Coloring

Existential

Grounding

IndependentSet

Projection

Reduction

MachineLearning

UniformLearning

AC0

Basic

KushilevitzMansour

LowDegree

MembershipQuery

Probability

ApproximateCounting (file)

Relative

BitString (file)

LinearHash (file)

Collisions

List (file)

All

Vote

SubsetSum (file)

Matrix

AffineHash

HashFamily (file)

MultiplyShift

Polynomial

KWiseIndependent (file)

Polynomial

MinEntropy (file)

Flat

LeftoverHash

PMF (file)

Bind

Event

Expect

Map

Uniform

PairwiseIndependentHash (file)

Affine

Shift

Toeplitz

Universal

SmallBias (file)

Powering

StatisticalDistance (file)

Product

UniformMod

AdaptiveWeights

BoundedDifferences

Chernoff

Collision

Concentration

Conditioning

Divergence

Entropy

EntropyConcentration

EntropyExtraction

Forking

Guessing

HashIsolation

IID

Isolation

LocalLemma

LoomisWhitney

Minimax

PairwiseIndependent

Pinsker

Product

Quantile

RejectionSampling

Rewinding

Shearer

Uniform

UniformNat

UniversalHash

Tactic

FirstOrder (file)

Init

PolyTime (file)

Init

Stateful (file)

Init

PPT

Synthesis

WordRAM

Init

Cslib

Computability

Circuit

Boolean

Basic

Complexity

Counting

Lupanov

LupanovConstruction

Shannon

Synthesis

Basic

Complexity

Composition

Counting

Depth

Finite

Full

Homomorphism

Normalization

Program

RelativeComplexity

Shannon

Signature

Simulation

Synthesis

Wire

Languages

Slice

Machines

Turing

MultiTape

Combinators

AlmostConstant

Id

Plumbing

Tidy

Defs

ClearWork

ExtendTapes

ForwardWork

InputFromTape

OutputToTape

RepeatUntilBlank

RewindInput

RewindWork

Sequential

TransformsTapes

WordsCfg

ConfigBound

Configuration

Deterministic

Nondeterministic

Space

TapeLemmas

SingleTape

Deterministic

QueryComplexity

Defs

Measures

URM

Basic

Defs

Crypto

Primitives

PRG

Asymptotic

Basic

Defs

Negligible

Foundations

Control

Monad

IsMonadHom (file)

List

Data

Fin

Tuple

List

IsChainFromTo

Nat

Asymptotics

Factorial

PolynomialBound

PFunctor

Free

Polynomial

Monotone

BiTape

BitString

StackTape

Lint

Basic

Relation

Defs

RelatesInSteps

Semantics

LTS

Basic

MachineLearning

PACLearning

Defs

Probability

PMF

StatisticalDistance

Tactic

GrindAttrs

Init

ImportGraph

Graph

TransitiveClosure

Imports

FromSource

ImportGraph

Pretty

Redundant

RequiredModules

Lean

EnvExtension

Environment

Json

MessageData

Syntax

Shake

Algebra

Basic

Core

DeclNeeds

EnvExtension

Environment

Workspace

Tools (file)

FindHome

ImportDiff

MinImports

NormImports

RedundantImports

Util

Modules

Widget

Collapsible

Copy

GoToModule

WorkspaceModel

Summary (file)

Cache

Core

Get

Base

Build

Model

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

Package

Perm

Range

Set

TakeDrop

Zip

BitVec (file)

Basic

BasicAux

Bitblast

Bootstrap

Decidable

Folds

Lemmas

Package

ByteArray (file)

Basic

Bootstrap

Extra

Lemmas

Lex

Char (file)

Basic

Lemmas

Order

Ordinal

Dyadic (file)

Basic

Instances

Inv

Round

Fin (file)

Basic

Bitwise

Fold

Iterate

Lemmas

Log2

MinMax

OverflowAware

Package

Float (file)

Model (file)

Format (file)

Basic

Valid

Unpacked (file)

Operations (file)

Add

Compare

Div

Fma

MinMax

Mul

OfNat

OfScientific

Sign

Sqrt

Status

Sub

ToNat

Pack (file)

Basic

Lemmas

Basic

Round

Sign

Float

Float32

Float

Float32

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

Package

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

Package

Pairwise

Perm

Range

Sublist

TakeDrop

ToArray

ToArrayImpl

Zip

Nat (file)

Bitwise (file)

Basic

Lemmas

Div (file)

Basic

Lemmas

Internal (file)

Linear

SOM

Power2 (file)

Basic

Bitwise

Lemmas

Sqrt (file)

Basic

Lemmas

Basic

Compare

Control

Coprime

Dvd

Fold

Gcd

Lcm

Lemmas

Log2

MinMax

Mod

Order

Package

PowMod

Simproc

ToString

OfScientific (file)

Basic

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

Decidable

Float

Float32

IntToBitVec

Lemmas

Package

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

Decode

FindPos

Hashable

Intercalate

IsEmpty

Iter

Iterate

Length

Lossy

Modify

Order

Search

Slice

Splits

StringOrder

TakeDrop

Pattern (file)

Basic

Char

Pred

String

Basic

Bootstrap

Compare

Csimp

Decode

Defs

Extra

FindPos

Hashable

Iterate

Iterator

Legacy

Length

Lossy

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

Decidable

IntToBitVec

Lemmas

Log2

Package

Vector (file)

Algebra

Attach

Basic

Count

DecidableEq

Erase

Extract

FinRange

Find

InsertIdx

Int

Lemmas

Lex

MapIdx

Monadic

Nat

OfFn

Package

Perm

Range

Stream

Zip

AC

BEq

Bool

Cast

Erased

Function

Hashable

LawfulHashable

NeZero

PLift

Prod

Queue

RArray

Random

Repr

Stream

ULift

Zero

Grind (file)

Homo (file)

BitVec

Extra

Fin

ISize

Int16

Int32

Int64

Int8

UInt16

UInt32

UInt64

UInt8

USize

Module (file)

Basic

Envelope

NatModuleNorm

OfNatModule

Ordered (file)

Field

Int

Linarith

Module

Order

Rat

Ring

Ring (file)

Basic

CommSemiringAdapter

CommSolver

Envelope

Field

FieldSolver

IntSolver

OfScientific

AC

Annotated

Attr

Cases

Config

Ext

FieldNormNum

Injective

Interactive

Lemmas

Lint

Norm

Offset

Order

PP

Propagator

Tactics

ToInt

Util

GrindInstances (file)

Ring (file)

BitVec

Fin

Int

Nat

Rat

SInt

UInt

Nat

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

LetFun

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

Trace

Config

Glob

Util

Date

String

Version

Lean (file)

Compiler

IR (file)

Basic

Checker

CompilerM

EmitLLVM

EmitUtil

Format

LLVMBindings

Meta

NormIds

Sorry

ToIR

ToIRType

UnboxResult

LCNF

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

ExpandResetReuse

ExplicitBoxing

ExplicitRC

ExtractClosed

FVarUtil

FixedParams

FloatLetIn

InferBorrow

InferType

Internalize

Irrelevant

JoinPoints

LCtx

LambdaLifting

Level

LiveVars

Main

MonadScope

MonoTypes

OtherDecl

PassManager

Passes

PhaseExt

PrettyPrinter

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

ImplementedByAttr

InitAttr

InlineAttrs

MetaAttr

ModPkgExt

NameMangling

NeverExtractAttr

NoncomputableAttr

Old

Options

Specialize

Data

Html

Basic

CharRef

Elab

Spec

Syntax

Iterators

Producers

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

Basic

Array

AssocList

DeclarationRange

Format

FuzzyMatching

JsonRpc

KVMap

LBool

LOption

Name

NameTrie

OpenDecl

Options

PPContext

PersistentArray

PersistentHashMap

PersistentHashSet

Position

PrefixTree

RArray

RBTree

SMap

SSet

Trie

DocString (file)

Add

DeferredCheck

Extension

Formatter

Links

Markdown

Parser

Syntax

Types

View

Elab (file)

BuiltinDo

Repeat

Command (file)

Scope

ConfigEval (file)

Basic

Commands

DeriveEvalConfigItem

DeriveEvalExpr

DeriveEvalTerm

Extra

Instances

MetaInstances

Types

Util

Deriving

Basic

Util

Do (file)

Basic

Control

ForwardSyntax

InferControlInfo

Legacy

PatternVar

Switch

DocString (file)

Builtin (file)

Postponed

Scopes

InfoTree (file)

Basic

InlayHints

Main

Types

Util

PreDefinition

PartialFixpoint (file)

Eqns

Induction

Main

Structural (file)

BRecOn

Basic

Eqns

FindRecArg

IndGroupInfo

IndPred

Main

Preprocess

RecArgInfo

SmartUnfolding

WF

Basic

Eqns

Fix

FloatRecApp

GuessLex

Main

PackMutual

Preprocess

Rel

Unfold

Basic

EqnsUtils

FixedParams

Main

MkInhabitant

Mutual

TerminationHint

TerminationMeasure

Quotation (file)

Precheck

Util

Tactic

Conv

Basic

Pattern

Simp

Grind

Anchor

Annotated

Basic

Config

Main

Param

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

VCGen (file)

AutoTry

Basic

BuiltinTactic

Calc

Classical

Config

Doc

ElabTerm

Ext

FalseOrByContra

Induction

LibrarySearch

Location

Meta

Monotonicity

RCases

RenameInaccessibles

Rewrite

Simp

SimpTrace

SolveByElim

Split

Try

Term (file)

TermElabM

App

Arg

AssertExists

Attributes

AutoBound

AuxDef

Binders

BindersUtil

BuiltinCommand

BuiltinNotation

BuiltinTerm

Calc

Coinductive

ComputedFields

Config

DeclModifiers

DeclNameGen

DeclUtil

Declaration

DeclarationRange

DefView

DeprecatedArg

DeprecatedSyntax

ElabRules

ErrorUtils

Eval

Exception

Extra

Import

Level

MacroArgUtil

Match

MatchAltView

MutualDef

MutualInductive

Open

Parallel

ParseImportsFast

PatternVar

RecAppSyntax

SetOption

Syntax

SyntheticMVars

Task

Util

WhereFinally

Language

Lean

Types

Util

Basic

LibrarySuggestions

Basic

Default

SineQuaNon

SymbolFrequency

Linter (file)

CodeQuality

Basic

AmbiguousOpen

Basic

Deprecated

Init

MissingDocs

PersistentLintLog

Sets

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

MatcherApp (file)

Basic

Transform

AltTelescopes

Basic

CaseArraySizes

CaseValues

MVarRenaming

Match

MatchEqsExt

MatchPatternAttr

MatcherInfo

NamedPatterns

SimpH

SolveOverlap

Value

Sym

Arith

Classify

DenoteExpr

EvalNum

Functions

Insts

MonadCanon

MonadRing

MonadSemiring

MonadVar

Norm

Poly

SafePoly

ToExpr

Types

VarRename

DSimp (file)

App

DSimpM

DSimproc

EvalGround

Forall

Lambda

Let

Main

Reduce

Result

Rewrite

Variant

Simp

App

Arith

Attr

CongrInfo

ControlFlow

Discharger

DiscrTree

EvalGround

Forall

Have

Lambda

Main

Reduce

Result

Rewrite

SimpM

Simproc

Theorems

AbstractS

AlphaShareBuilder

AlphaShareCommon

Apply

Canon

Eta

ExprPtr

InferType

InstantiateMVarsS

InstantiateS

IsClass

LitValues

LooseBVarsS

MaxFVar

Offset

Pattern

ProofInstInfo

Reduce

ReplaceS

SymM

SynthInstance

Util

Tactic

Grind

AC

DenoteExpr

PP

Seq

Types

Util

Arith

CommRing

DenoteExpr

PP

RingId

RingM

Types

Cutsat

Model

Types

Util

Linear

LinearM

Model

PP

Reify

StructId

Types

Util

Var

FieldNormNum

IsRelevant

ModelUtil

Simproc

Util

Action

Anchor

Attr

Beta

Cases

CasesMatch

CastLike

CheckResult

CollectParams

Core

Ctor

CtorIdx

EMatch

EMatchAction

EMatchDiagnostics

EMatchTheorem

EMatchTheoremParam

EMatchTheoremPtr

EqResolution

ExtAttr

Extension

Finish

ForallAnd

ForallProp

Homo

Injection

Injective

Internalize

Intro

Inv

LawfulEqCmp

Main

MarkAccessible

MarkNestedSubsingletons

MatchCond

MatchDiscrOnly

NormSym

NormSymProcs

Normalizer

PP

Parser

Proj

Proof

PropagateInj

PropagatorAttr

ProveEq

ReflCmp

RegisterCommand

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

FunIndCollect

FunIndInfo

Generalize

IndependentOf

Induction

Injection

Intro

LibrarySearch

NormCast

Refl

Rename

Repeat

Replace

Revert

Rewrite

Rfl

SolveByElim

Split

SplitIf

Subst

Symm

TryThis

UnifyEq

Util

ACLt

AbstractMVars

AbstractNestedProofs

AppBuilder

Basic

BinderNameHint

Canonicalizer

CasesInfo

Check

Closure

Coe

CoeAttr

CollectFVars

CollectMVars

CompletionName

CongrTheorems

CtorIdxHInj

CtorRecognizer

DecLevel

Diagnostics

Eqns

Eval

ExprLens

ForEachExpr

FunInfo

GeneralizeTelescope

GeneralizeVars

GetUnfoldableConst

HasAssignableMVar

HasNotBit

HaveTelescope

Hint

IndPredBelow

InferType

Injective

Instances

IntInstTesters

Iterator

KAbstract

KExprMap

LazyDiscrTree

LetToHave

LitValues

MatchUtil

MethodSpecs

MkIffOfInductiveProp

MonadSimp

NatInstTesters

NatTable

Offset

Order

PPBinder

PPGoal

PProdN

ProdN

RecExt

RecursorInfo

Reduce

ReduceEval

SameCtorUtils

SizeOf

Sorry

StringLitProof

Structure

SynthInstance

Transform

TransparencyMode

TryThis

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

CodeActions (file)

Attr

Basic

Provider

Completion (file)

CompletionCollectors

CompletionInfoSelection

CompletionItemCompression

CompletionResolution

CompletionUtils

EligibleHeaderDecls

SyntheticCompletion

FileWorker

ExampleHover

InlayHints

RequestHandling

SemanticHighlighting

SignatureHelp

Utils

Rpc

Basic

RequestHandling

Test

Cancel

AsyncList

FileSource

GoTo

References

RequestCancellation

Requests

ServerTask

Snapshots

Utils

Util

CollectAxioms

CollectFVars

CollectLevelMVars

CollectLevelParams

CollectLooseBVars

CollectMVars

Diff

FindExpr

FindLevelMVar

FindMVar

FoldConsts

ForEachExpr

ForEachExprWhere

HasConstCache

Heartbeats

InstantiateLevelParams

LeanOptions

MonadBacktrack

MonadCache

NumApps

NumObjs

OccursCheck

PPExt

ParamMinimizer

Path

Profile

PtrSet

RecDepth

Recognizers

ReplaceExpr

ReplaceLevel

SCC

SafeExponentiation

ShareCommon

Sorry

SortExprs

Trace

UnusedBinders

Widget

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

ReservedNameAction

ResolveName

Runtime

ScopedEnvExtension

Setup

Structure

SubExpr

Syntax

ToExpr

ToLevel

LeanSearchClient (file)

Basic

LoogleSyntax

Syntax

Mathlib

Algebra

Algebra

Spectrum

Basic

Pi

Quasispectrum

Subalgebra

Basic

Directed

IsSimpleOrder

Lattice

Operations

Pointwise

Prod

Tower

Basic

Bilinear

Defs

Equiv

Hom

IsSimpleRing

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Rat

RestrictScalars

StrictPositivity

Tower

TransferInstance

Unitization

ZMod

BigOperators

Finsupp

Basic

Fin

Group

Finset

Basic

Defs

Gaps

Indicator

Lemmas

Pi

Piecewise

Powerset

Preimage

Sigma

List

Basic

Defs

Lemmas

Multiset

Basic

Defs

GroupWithZero

Action

Finset

Ring

Finset

List

Multiset

Nat

Associated

Balance

Expect

Field

Fin

Finprod

Intervals

Module

NatAntidiagonal

Option

Pi

RingEquiv

WithTop

Category

Grp

Basic

ForgetCorepresentable

Limits

Preadditive

MonCat

Basic

ForgetCorepresentable

Limits

Ring

Adjunctions

Basic

Colimits

Constructions

Instances

Limits

Central

Basic

Defs

CharP

Algebra

Basic

Defs

Frobenius

IntermediateField

Invertible

Lemmas

Reduced

Two

CharZero

AddMonoidHom

Defs

Infinite

Quotient

DirectSum

Algebra

Basic

Decomposition

Finsupp

Internal

Module

Ring

Divisibility

Basic

Hom

Units

EuclideanDomain

Basic

Defs

Field

Int

Exact

Basic

Field

Subfield

Basic

Defs

Basic

Defs

Equiv

GeomSum

IsField

NegOnePow

Opposite

Periodic

Rat

TransferInstance

ZMod

FiniteSupport

Basic

Defs

FreeAbelianGroup

Finsupp

FreeMonoid

Basic

UniqueProds

GCDMonoid

Basic

Finset

FinsetLemmas

IntegrallyClosed

Multiset

Nat

Group

Action

Pointwise

Set

Basic

Finset

Basic

Defs

End

Faithful

Hom

Opposite

Pi

Pretransitive

Prod

TransferInstance

TypeTags

Units

Commute

Basic

Defs

Hom

Units

Equiv

Basic

Defs

Opposite

TypeTags

Fin

Basic

Tuple

Hom

Basic

CompTypeclasses

Defs

End

Instances

Int

Defs

Even

Units

Invertible

Basic

Defs

Irreducible

Defs

Lemmas

Nat

Defs

Even

Hom

Units

Pi

Basic

Lemmas

Torsion

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

Finsupp

Ker

Lattice

Map

MulOpposite

MulOppositeLemmas

Order

Pointwise

Submonoid

Basic

BigOperators

Defs

DistribMulAction

Finite

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

DivInvMonoid

Embedding

End

Even

EvenFunction

Finsupp

FunLike

Graph

Idempotent

Indicator

InjSurj

IsApply

IsCommutative

ModEq

Monoid

NatPowAssoc

Opposite

PUnit

Prod

SelfInv

Semigroup

Shrink

Support

Torsion

TransferInstance

ULift

GroupWithZero

Action

Pointwise

Set

Basic

Defs

End

Hom

Opposite

Pi

Prod

Regular

TransferInstance

Units

Pointwise

Set

Basic

Submonoid

Instances

Pointwise

Primal

Units

Basic

Equiv

Fintype

Lemmas

Associated

Basic

Center

Commute

Defs

Divisibility

Equiv

FunLike

Hom

Idempotent

Indicator

InjSurj

Invertible

Nat

NeZero

NonZeroDivisors

Opposite

Pi

Prod

Range

Regular

Semiconj

Subgroup

ULift

WithZero

Module

Congruence

Defs

Equiv

Basic

Defs

Opposite

LinearMap

Basic

Defs

DivisionRing

End

Prod

Star

LocalizedModule

Basic

IsLocalization

Submodule

Submodule

Basic

Bilinear

Defs

EqLocus

Equiv

Finsupp

Invariant

IterateMapComap

Ker

Lattice

LinearMap

Map

Pointwise

Range

RestrictScalars

Torsion

Basic

Field

Free

Pi

Basic

BigOperators

Defs

End

FunLike

Hom

MinimalAxioms

NatInt

Opposite

PUnit

Pi

Prod

Projective

Rat

RingHom

Shrink

SpanRank

TransferInstance

ULift

ZMod

MonoidAlgebra

Basic

Cardinal

Defs

Degree

Division

Lift

MapDomain

Module

NoZeroDivisors

Opposite

Support

MvPolynomial

Basic

Coeff

CommRing

Degrees

Derivation

Equiv

Eval

Expand

Funext

Monad

Nilpotent

PDeriv

Polynomial

Rename

SchwartzZippel

Supported

Variables

NoZeroSMulDivisors

Basic

Defs

Notation (file)

Pi

Basic

Defs

Bracket

Defs

FiniteSupport

Indicator

Lemmas

Prod

Support

Order

AbsoluteValue

Basic

Int

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

GeomSum

Power

Rat

Floor

Defs

Div

Ring

Semifield

Semiring

Group

Action (file)

Synonym

Pointwise

Bounds

CompleteLattice

Interval

Unbundled

Abs

Basic

Int

Abs

Basic

Cyclic

Defs

DenselyOrdered

Finset

Indicator

Int

Lattice

MinMax

Multiset

Nat

Opposite

OrderIso

PiLex

PosPart

Synonym

Units

GroupWithZero

Action

Synonym

Basic

Canonical

Defs

Finset

OrderIso

Range

Submonoid

Synonym

WithZero

Hom

Basic

GroupNorm

Monoid

MonoidWithZero

Ring

RingNorm

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

Multiset

NatCast

OrderDual

Prod

Submonoid

TypeTags

Units

WithTop

Nonneg

Basic

Field

Floor

Lattice

Module

Ring

Positive

Ring

Ring

Unbundled

Basic

Rat

Abs

Basic

Canonical

Cast

Defs

Finset

GeomSum

Idempotent

InjSurj

Int

Interval

IsNonarchimedean

NNRat

Nat

Pow

Rat

Star

Synonym

WithTop

Star

Basic

Pi

Prod

Real

Sub

Unbundled

Basic

Basic

Defs

WithTop

SuccPred (file)

PartialSups

WithBot

AddGroupWithTop

AddTorsor

Algebra

Chebyshev

Invertible

IsBotOne

Kleene

Monovary

Pi

Rearrangement

Round

ToIntervalMod

ZeroLEOne

Polynomial

Degree

Defs

Domain

IsMonicOfDegree

Lemmas

Monomial

Operations

SmallDegree

Support

TrailingDegree

Units

Eval

Algebra

Coeff

Defs

Degree

SMul

Subring

Module

AEval

Basic

AlgebraMap

Basic

BigOperators

Bivariate

CancelLeads

Coeff

CoeffList

Derivation

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Monic

Monomial

Reverse

RingDivision

Roots

Sequence

Smeval

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

BooleanRing

Center

Centralizer

CharZero

Commute

CompTypeclasses

Defs

Equiv

Fin

FunLike

GeomSum

GrindInstances

Idempotent

InjSurj

Invertible

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

FreeAlgebra

GradedMonoid

GradedMulAction

IsPrimePow

NeZero

Opposites

QuadraticDiscriminant

Quotient

Analysis

Analytic

Basic

CPolynomial

CPolynomialDef

ChangeOrigin

Composition

Constructions

ConvergenceRadius

Inverse

IsolatedZeros

Linear

OfScalars

Uniqueness

Within

Asymptotics

Arith

AsymptoticEquivalent

Basic

Defs

Lemmas

Prod

Ring

SpecificAsymptotics

SuperpolynomialDecay

TVS

Theta

BoxIntegral

Box

Basic

SubboxInduction

Partition

Additive

Basic

Filter

Measure

Split

SubboxInduction

Tagged

Basic

DivergenceTheorem

Integrability

CStarAlgebra

ContinuousFunctionalCalculus

Commute

Continuity

Instances

Isometric

NonUnital

Pi

Restrict

Unique

Unital

Basic

Classes

Matrix

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

Prod

Shift

Slope

Support

ZPow

FDeriv

Add

Affine

Analytic

Basic

Bilinear

Comp

CompCLM

Congr

Const

Defs

Equiv

Extend

Linear

Measurable

Mul

OfCompLeft

Pow

Prod

RestrictScalars

WithLp

InverseFunctionTheorem

ApproximatesLinearOn

Deriv

FDeriv

IteratedDeriv

Defs

Lemmas

LocalExtr

Basic

Rolle

TangentCone

Basic

Defs

DimOne

Prod

Real

DSlope

DiffContOnCl

FormalMultilinearSeries

LagrangeMultipliers

LogDeriv

MeanValue

Monotone

ParametricIntegral

ParametricIntervalIntegral

Taylor

Complex

Polynomial

Basic

Arg

Asymptotics

Basic

Cardinality

CauchyIntegral

Circle

Convex

Exponential

ExponentialBounds

IsIntegral

Liouville

Norm

Order

ReImTopology

RealDeriv

Spectrum

Trigonometric

Convex

Cone

Extension

SpecificFunctions

Basic

Deriv

Approximation

Basic

Between

Combination

Continuous

Deriv

EGauge

Function

Gauge

Hull

Integral

Intrinsic

Jensen

Mul

PathConnected

Quasiconvex

Segment

Side

Slope

Star

StdSimplex

Strict

StrictConvexSpace

Topology

Uniform

Fourier

FiniteAbelian

Orthogonality

BoundedContinuousFunctionChar

FourierTransform

Notation

InnerProductSpace

Projection

Basic

FiniteDimensional

Minimal

Reflection

Submodule

Adjoint

Basic

Calculus

Continuous

Convex

Defs

Dual

GramMatrix

GramSchmidtOrtho

LinearMap

Orientation

Orthogonal

Orthonormal

PiL2

Positive

ProdL2

Rayleigh

Spectrum

Subspace

Symmetric

TwoDim

LocallyConvex

BalancedCoreHull

Basic

Bounded

ContinuousOfBounded

HahnBanach

SeparatingDual

Separation

WeakDual

WithSeminorms

Matrix

Hermitian

HermitianFunctionalCalculus

MeasurableSpace

Normed

Order

PosDef

Spectrum

Normed

Affine

AddTorsor

AddTorsorBases

Convex

Isometry

Algebra

Exponential

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

RadialFunction

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

Seminorm

Basic

Norm

Basic

Completion

Convex

FiniteDimension

HahnBanach

Normalize

Ray

RieszLemma

Span

Operator

Compact

Basic

FiniteDimension

FredholmAlternative

Asymptotics

Banach

Basic

Bilinear

BoundedLinearMaps

CompleteCodomain

ContinuousLinearMap

Extend

LinearIsometry

Mul

NNNorm

NormedSpace

Order

Lattice

Ring

Basic

Finite

InfiniteSum

Lemmas

Units

MulAction

Polynomial

Basic

RCLike

Basic

BoundedContinuous

Extend

Inner

Lemmas

Sqrt

Real

Pi

Bounds

Cardinality

Spectrum

Sqrt

SpecialFunctions

Complex

Analytic

Arg

Circle

CircleMap

Log

LogBounds

LogDeriv

ContinuousFunctionalCalculus

PosPart

Basic

Rpow

Basic

Isometric

Measurable

Abs

Gamma

Basic

Gaussian

FourierTransform

GaussianIntegral

Integrability

Basic

Integrals

Basic

Log

Base

Basic

Deriv

InvLog

NegMulLog

Pow

Asymptotics

Complex

Continuity

Deriv

NNReal

NthRootLemmas

Real

Trigonometric

Chebyshev

Basic

RootsExtrema

Angle

Arctan

ArctanDeriv

Basic

Bounds

Complex

ComplexDeriv

Deriv

DerivHyp

Inverse

InverseDeriv

Series

Sinc

Arcosh

Bernstein

Exp

ExpDeriv

Exponential

ImproperIntegrals

JapaneseBracket

MulExpNegMulSq

MulExpNegMulSqIntegral

NonIntegrable

PolarCoord

Sqrt

SpecificLimits

ArithmeticGeometric

Basic

Normed

RCLike

BoundedVariation

LConvolution

MeanInequalities

MeanInequalitiesPow

Oscillation

Basic

Complex

Basic

BigOperators

Countable

Basic

Defs

Small

ENNReal

Action

Basic

BigOperators

Holder

Inv

Lemmas

Operations

Real

Finite

Defs

Prod

Set

Sigma

Sum

FunLike

Basic

Embedding

Equiv

IsEmpty

Basic

Defs

Logic

Basic

Lemmas

NNReal

Basic

Defs

Star

Nontrivial

Basic

Defs

Real

Basic

ConjExponents

ENatENNReal

Pointwise

Star

Rel (file)

Cover

Separated

SetLike

Basic

Sign

Basic

Defs

Denumerable

ExistsUnique

Nonempty

Opposite

SProd

Unique

UnivLE

CategoryTheory

Adjunction

Basic

FullyFaithful

Limits

Mates

Bicategory

Strict

Basic

Basic

Category

Cat (file)

AsSmall

Basic

Init

Preorder

ULift

Comma

Over

Basic

Pullback

StructuredArrow

Basic

Arrow

Basic

ConcreteCategory

Basic

Bundled

Elementwise

Forget

Notation

ReflectsIso

Discrete

Basic

EffectiveEpi

Basic

Filtered

Basic

Connected

FinCategory

AsType

Basic

Functor

ReflectsIso

Basic

Basic

Category

Const

Currying

EpiMono

FullyFaithful

Hom

TwoSquare

LiftingProperties

Adjunction

Basic

Limits

ConcreteCategory

Basic

Constructions

BinaryProducts

FunctorCategory

Basic

Preserves

Shapes

Pullbacks

Terminal

Zero

Basic

Limits

Ulift

Shapes

BinaryProducts

BinaryFan

BinaryProducts

WalkingPair

Opposites

Equalizers

Pullbacks

Pullback

IsPullback

Basic

Defs

Assoc

Cospan

HasPullback

Iso

Mono

Pasting

PullbackCone

Diagonal

Equalizers

FiniteLimits

Grothendieck

Images

IsTerminal

KernelPair

Kernels

Products

RegularMono

StrictInitial

StrongEpi

Terminal

WidePullbacks

ZeroMorphisms

ZeroObjects

Types

ColimitType

Colimits

Filtered

Images

Limits

Products

Cones

Connected

Creates

Final

HasLimits

IsLimit

Opposites

Yoneda

Monad

Algebra

Basic

Products

MorphismProperty

Basic

Composition

Factorization

Limits

ObjectProperty

Basic

ClosedUnderIsomorphisms

CompleteLattice

Equivalence

FullSubcategory

Opposite

Small

Pi

Basic

Preadditive

Basic

Products

Basic

Unitor

Types

Basic

Balanced

CommSq

Elements

Elementwise

Endomorphism

EpiMono

EqToHom

Equivalence

EssentialImage

EssentiallySmall

Grothendieck

Groupoid

HomCongr

InducedCategory

IsConnected

Iso

IsomorphismClasses

NatIso

NatTrans

Opposites

PEmpty

PUnit

Retract

ShrinkYoneda

Skeletal

Thin

Whiskering

Yoneda

Combinatorics

Digraph

Basic

Enumerative

Partition

Basic

Composition

DoubleCounting

InclusionExclusion

Stirling

Graph

Connected

EdgeCut

Basic

Delete

Subgraph

Hall

Finite

Matroid

Minor

Restrict

Rank

Cardinal

ENat

Finite

Basic

Circuit

Closure

Constructions

Dual

IndepAxioms

Init

Loop

Map

Quiver

Basic

Path

Prefunctor

Push

Symmetric

SetFamily

Compression

Down

Shatter

SimpleGraph

Coloring

Vertex

Connectivity

Connected

EdgeConnectivity

Finite

Subgraph

Walk

Basic

Chord

Counting

Decomp

Maps

Operations

Subwalks

Traversal

Acyclic

Basic

Bipartite

Clique

Copy

CycleGraph

Dart

DegreeSum

DeleteEdges

Density

Finite

Hamiltonian

Hasse

Init

Maps

Metric

Operations

Paths

Prod

Subgraph

Sum

VertexCover

Colex

Nullstellensatz

Pigeonhole

Computability

Primrec

Basic

List

TuringMachine

Computable

PostTuringMachine

StackTuringMachine

Tape

Encoding

Language

Partrec

PartrecCode

RE

Reduce

StateTransition

Control

Monad

Basic

Cont

Writer

Traversable

Basic

Applicative

Basic

Bifunctor

Combinators

EquivFunctor

Functor

Lawful

ULift

ULiftable

Data

Bool

Basic

Set

DFinsupp

BigOperators

Defs

Ext

Lex

Module

NeLocus

Order

Sigma

Small

Submonoid

WellFounded

ENat

Basic

Defs

Lattice

Monoid

Pow

EReal

Basic

Inv

Operations

Fin

Tuple

Basic

Embedding

Finset

NatAntidiagonal

Reflection

Sort

Take

Basic

Embedding

Rev

SuccPred

VecNotation

FinEnum (file)

Option

Finite

Perm

Finset

Lattice

Basic

Fold

Lemmas

Prod

Union

Attach

Attr

Basic

BooleanAlgebra

Card

Dedup

Defs

Density

Disjoint

Empty

Erase

Filter

Fin

Fold

Image

Insert

Max

MulAntidiagonal

NAry

NatAntidiagonal

NoncommProd

Option

Order

Pairwise

Pi

Piecewise

Powerset

Preimage

Prod

Range

SDiff

SMulAntidiagonal

Sigma

Slice

Sort

Sum

Sym

SymmDiff

Union

Update

Finsupp

MonomialOrder (file)

DegLex

Antidiagonal

Basic

Defs

Ext

Fin

Fintype

Indicator

Lex

Multiset

Option

Order

PWO

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

Sigma

Sort

Sum

Vector

FunLike

Fintype

Int

Cast

Basic

Defs

Field

Lemmas

Pi

Prod

Order

Basic

Units

Basic

CardIntervalMod

CharZero

DivMod

GCD

Init

Interval

Log

ModEq

Notation

Sqrt

WithZero

List

Perm

Basic

Lattice

Subperm

AList

Basic

Chain

Count

Cycle

Dedup

Defs

DropRight

Duplicate

Enum

FinRange

Find

Flatten

Forall2

GetD

Indexes

Induction

Infix

InsertIdx

Iterate

Lattice

Lex

Lookmap

MinMax

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

OffDiag

Pairwise

Permutation

Pi

Prime

ProdSigma

Range

Rotate

Sigma

Sort

SplitLengths

Sublists

Sym

TFAE

TakeDrop

TakeWhile

ToFinsupp

Zip

Matrix

Basic

Basis

Block

ColumnRowPartitioned

Composition

Diagonal

Mul

Reflection

Multiset

AddSub

Antidiagonal

Basic

Bind

Count

Dedup

Defs

Filter

Find

FinsetOps

Fintype

Fold

Lattice

MapFold

NatAntidiagonal

Pi

Powerset

Range

Replicate

Sections

Sort

Sum

Sym

UnionInter

ZeroCons

NNRat

Defs

Nat

Cast

Order

Basic

Field

Ring

Basic

Commute

Defs

Field

NeZero

Pi

Prod

WithTop

Choose

Basic

Bounds

Cast

Central

Dvd

Factorization

Multinomial

Sum

Vandermonde

Digits

Defs

Lemmas

Factorial

Basic

BigOperators

Cast

DoubleFactorial

SuperFactorial

Factorization

Basic

Defs

Induction

LCM

PrimePow

GCD

Basic

BigOperators

NthRoot

Defs

Order

Lemmas

Prime

Basic

Defs

Factorial

Infinite

Int

Nth

Pow

Basic

BinaryRec

BitIndices

Bits

Bitwise

ChineseRemainder

Count

Dist

Factors

Find

Init

Log

MaxPowDiv

ModEq

Multiplicity

Notation

Nth

PSub

PadicValNat

Pairing

Periodic

PrimeFin

Set

Size

Sqrt

Squarefree

Totient

WithBot

Num

Basic

Bitwise

Lemmas

Option

Basic

Defs

NAry

Ordering

Basic

PFunctor

Univariate

Basic

PNat

Basic

Defs

Equiv

Notation

Prime

Prod

Basic

PProd

TProd

Rat

Cast

CharZero

Defs

Lemmas

Order

BigOperators

Defs

Encodable

Floor

Init

Lemmas

Sqrt

Seq

Computation

Set

Card (file)

Arithmetic

Finite

Basic

Lattice

Lemmas

List

Powerset

Range

Lattice

Bounded

Disjoint

Image

Indexed

Order

Pairwise

Basic

Lattice

List

Basic

BoolIndicator

BooleanAlgebra

CoeSort

Constructions

Countable

Defs

Disjoint

Function

Functor

Image

Inclusion

Insert

List

MemPartition

Monotone

MulAntidiagonal

NAry

Notation

Operations

Order

Piecewise

Prod

Restrict

SMulAntidiagonal

Semiring

Sigma

Subset

Subsingleton

SymmDiff

UnionLift

SetLike

Fintype

Sigma

Basic

Stream

Defs

Init

String

Defs

Sum

Basic

Sym

Sym2 (file)

Init

Basic

Card

Tree

Basic

Vector

Basic

Defs

W

Basic

Cardinal

ZMod

Aut

Basic

Defs

IntUnitsPower

QuotientGroup

QuotientRing

Units

ValMinAbs

BitVec

Bundle

Ineq

PFun

Part

Quot

Subtype

ULift

Dynamics

Ergodic

MeasurePreserving

FixedPoints

Basic

Defs

PeriodicPts

Defs

Lemmas

Minimal

FieldTheory

Finite

Basic

GaloisField

Polynomial

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

Cardinality

Extension

Finiteness

Fixed

IsSepClosed

KrullTopology

KummerPolynomial

Perfect

PolynomialGaloisGroup

PrimitiveElement

Separable

SeparableClosure

SeparableDegree

Tower

Geometry

Convex

Cone

Basic

Pointed

ConvexSpace

AffineMap

Barycenter

CompactSpaceStdSimplex

Defs

Module

ModuleTopology

PathConnectedSpaceStdSimplex

Prod

Topology

Set

Star

Euclidean

Angle

Oriented

Affine

Basic

Rotation

Unoriented

Affine

Basic

TriangleInequality

Triangle

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

Cardinality

Divisibility

Maps

MonoidWithZero

OreLocalization

Basic

Cardinality

OreSet

Perm

Cycle

Basic

Concrete

Factors

Type

Basic

Closure

ConjAct

Fin

Finite

List

Option

Sign

Support

ViaEmbedding

QuotientGroup

Basic

Defs

Finite

ModEq

SpecificGroups

Cyclic (file)

Basic

Subgroup

Alternating

Subgroup

Center

Centralizer

Simple

Submonoid

Center

Centralizer

Subsemigroup

Center

Centralizer

Archimedean

Complement

DedekindFinite

Divisible

Exponent

Finiteness

FreeAbelianGroup

Index

IndexNormal

NoncommPiCoprod

OrderOfElement

PGroup

Rank

Solvable

Sylow

Torsion

InformationTheory

KullbackLeibler

Basic

ChainRule

DataProcessing

KLFun

Hamming

Lean

Elab

Tactic

Basic

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

Centroid

AffineEquiv

AffineMap

Basis

Centroid

Combination

Defs

Dimension

FiniteDimensional

Independent

Midpoint

Ordered

Pointwise

Restrict

Slope

Alternating

Basic

Curry

Basis

Basic

Bilinear

Cardinality

Defs

Fin

Prod

SMul

Submodule

VectorSpace

BilinearForm

Basic

DualLattice

Hom

Properties

Charpoly

BaseChange

Basic

ToMatrix

Complex

FiniteDimensional

Module

Orientation

Dimension

Basic

Constructions

DivisionRing

ErdosKaplansky

Finite

Finrank

Free

FreeAndStrongRankCondition

LinearMap

Localization

OrzechProperty

RankNullity

StrongRankCondition

Subsingleton

DirectSum

Finsupp

TensorProduct

Dual

Basis

Defs

Lemmas

Eigenspace

Basic

Charpoly

ContinuousLinearMap

Matrix

Minpoly

FiniteDimensional

Basic

Defs

Lemmas

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

Matrix

Basic

PID

StrongRankCondition

GeneralLinearGroup

AlgEquiv

Basic

LinearIndependent

Algebra

Basic

Defs

Lemmas

Matrix

Charpoly

Basic

Coeff

Eigs

LinearMap

Minpoly

Determinant

Bird

Correctness

Defs

Basic

GeneralLinearGroup

Defs

AbsoluteValue

Action

Adjugate

Basis

BilinearForm

Block

CharP

ConjTranspose

Defs

Diagonal

DotProduct

Dual

Hadamard

HadamardMatrix

Hermitian

Ideal

InvariantBasisNumber

Invertible

Kronecker

MvPolynomial

Nondegenerate

NonsingularInverse

Notation

Permanent

Polynomial

PosDef

Rank

Reindex

RowCol

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

StdBasis

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

Unique

Vec

ZPow

Multilinear

Basic

Basis

Curry

DFinsupp

Finsupp

QuadraticForm

Basic

Quotient

Basic

Card

Defs

SModEq

Basic

SesquilinearForm

Basic

Orthogonal

Span

Basic

Defs

TensorProduct

Associator

Basic

Basis

Defs

Finiteness

Lift

Map

Quotient

RightExactness

Tower

BilinearMap

Contraction

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

Sigma

Sum

Function

Basic

CompTypeclasses

Conjugate

Const

Defs

DependsOn

Iterate

ULift

Small

Basic

Defs

List

Set

OpClass

Pairwise

Relation

Relator

MeasureTheory

Constructions

BorelSpace

Basic

Complex

ContinuousLinearMap

Metric

Metrizable

Order

Real

WithTop

Polish

Basic

EmbeddingReal

StronglyMeasurable

Cylinders

Pi

Covering

Besicovitch

BesicovitchVectorSpace

DensityTheorem

Differentiation

OneDim

Vitali

VitaliFamily

Function

ConditionalExpectation

AEMeasurable

Basic

CondJensen

CondexpL1

CondexpL2

Indicator

LebesgueBochner

PullOut

RadonNikodym

Real

Unique

L1Space

AEEqFun

HasFiniteIntegral

Integrable

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

Defs

Indicator

LpNorm

Monotonicity

Prod

SMul

TriangleInequality

Trim

LpSpace

Basic

Complete

CompleteOfCompleteLp

ContinuousFunctions

Indicator

InfiniteSum

SpecialFunctions

Basic

StronglyMeasurable

AEStronglyMeasurable

Basic

ENNReal

Inner

Lemmas

Lp

AEEqFun

AEEqOfIntegral

AEEqOfLIntegral

AEMeasurableOrder

AEMeasurableSequence

AbsolutelyContinuous

ConditionalLExpectation

ConvergenceInMeasure

Egorov

EssSup

Floor

Holder

Jacobian

JacobianOneDim

L2Space

LocallyIntegrable

LpOrder

SimpleFunc

SimpleFuncDense

SimpleFuncDenseLp

UniformIntegrable

Group

Action

Arithmetic

Convolution

Defs

FundamentalDomain

Integral

IntegralConvolution

LIntegral

MeasurableEquiv

Measure

Pointwise

Prod

Integral

Bochner

Basic

ContinuousLinearMap

FundThmCalculus

L1

Set

SumMeasure

VitaliCaratheodory

IntervalIntegral

AbsolutelyContinuousFun

Basic

DerivIntegrable

FundThmCalculus

IntegrationByParts

LebesgueDifferentiationThm

Periodic

Slope

Lebesgue

Add

Basic

Countable

DominatedConvergence

Map

Markov

Norm

Sub

SetToL1

ChangeMeasure

DominatedConvergence

Function

L1

SimpleFunc

Asymptotics

Average

BoundedContinuousFunction

CircleIntegral

DivergenceTheorem

DominatedConvergence

ExpDecay

FinMeasAdditive

IntegrableOn

IntegralEqImproper

Layercake

Marginal

MeanInequalities

Pi

Prod

MeasurableSpace

Basic

Constructions

CountablyGenerated

Defs

Embedding

EventuallyMeasurable

Instances

MeasurablyGenerated

Pi

PreorderRestrict

Prod

Measure

CharacteristicFunction

Basic

Decomposition

Exhaustion

Hahn

IntegralRNDeriv

Lebesgue

RadonNikodym

Dirac

Basic

Def

Haar

Basic

InnerProductSpace

NormedSpace

OfBasis

Quotient

Unique

Lebesgue

Basic

Complex

EqHaar

Integral

TotalVariation

Basic

Defs

Typeclasses

Finite

NullSingletonClass

Probability

SFinite

ZeroOne

AEDisjoint

AEMeasurable

AbsolutelyContinuous

Basic

Comap

CompleteLattice

Complex

Content

Continuity

Count

Doubling

EverywherePos

Filter

FiniteMeasureExt

GiryMonad

HasOuterApproxClosed

Interval

LogLikelihoodRatio

Map

MeasureSpaceDef

Module

MutuallySingular

NullMeasurable

OpenPos

OuterMeasure

PreVariation

Prod

QuasiMeasurePreserving

Real

Regular

RegularityCompacts

Restrict

Stieltjes

Sub

Sum

Tilted

Trim

WithDensity

Order

Lattice

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfFunction

Operations

SpecificCodomains

Pi

WithLp

VectorMeasure

Decomposition

Hahn

Jordan

Lebesgue

RadonNikodym

Variation

Basic

Defs

Basic

Defs

Operations

Order

Relations

TotalVariation

WithDensity

PiSystem

Topology

ModelTheory

Basic

Bundled

Complexity

Definability

ElementaryMaps

ElementarySubstructures

Encoding

Equivalence

Graph

LanguageMap

Quotients

Satisfiability

Semantics

Skolem

Substructures

Syntax

Ultraproducts

NumberTheory

ArithmeticFunction

Defs

Misc

Moebius

VonMangoldt

Zeta

Cyclotomic

Basic

PrimitiveRoots

LegendreSymbol

AddCharacter

NumberField

Basic

Padics

PadicVal

Basic

Defs

Real

Irrational

AbelSummation

Bertrand

Chebyshev

Divisors

Niven

PrimeCounting

Primorial

Order

Atoms (file)

Finite

BooleanAlgebra

Basic

Defs

Set

BoundedOrder

Basic

Lattice

Monotone

Bounds

Basic

Defs

Image

OrderIso

CompactlyGenerated

Basic

Intervals

CompleteLattice

Basic

Chain

Defs

Finset

Group

Lemmas

ConditionallyCompleteLattice

Basic

Defs

Finset

Group

Indexed

ConditionallyCompletePartialOrder

Basic

Defs

Indexed

Defs

Lattice

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

OrderedMonoid

Ultrafilter

Basic

Defs

Basic

Cofinite

CountableInter

CountableSeparatingOn

CountablyGenerated

Curry

Defs

ENNReal

EventuallyConst

Extr

Finite

IndicatorFunction

Interval

IsBounded

Ker

Lift

Map

NAry

Pi

Pointwise

Prod

Ring

SmallSets

Subsingleton

Tendsto

TendstoCofinite

Fin

Basic

Tuple

GaloisConnection

Basic

Defs

Heyting

Basic

Boundary

Hom

Hom

Basic

Bounded

BoundedLattice

CompleteLattice

Lattice

Lex

Order

Set

WithTopBot

Int

ConditionallyCompleteOrder

LeastGreatest

Interval

Finset

Basic

Defs

Fin

Gaps

Nat

SuccPred

Set

Basic

Defs

Disjoint

Fin

Image

Infinite

LinearOrder

Monotone

OrdConnected

OrdConnectedComponent

OrderEmbedding

OrderIso

Pi

ProjIcc

SuccPred

UnorderedInterval

WithBotTop

Multiset

Lattice (file)

Nat

Monotone

Basic

Defs

Extension

Monovary

Odd

Union

Partition

Finpartition

Preorder

Chain

Finite

Finsupp

Prod

Lex

Basic

RelIso

Basic

Set

Setoid

Basic

Partition

Sigma

Lex

SuccPred

Archimedean

Basic

CompleteLinearOrder

ENat

Fin

InitialSeg

Int

IntervalSucc

Limit

LinearLocallyFinite

Nat

Relation

WithBot

Sum

Order

UpperLower

Basic

Closure

CompleteLattice

Fibration

Principal

Antichain

Antisymmetrization

Basic

BooleanSubalgebra

BourbakiWitt

Circular

Closure

Cofinal

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

Copy

Cover

DirSupClosed

Directed

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

Restriction

SaddlePoint

ScottContinuity

SetAccumulate

SetDissipate

SetNotation

Shrink

Sublattice

SupClosed

SupIndep

SymmDiff

TypeTags

ULift

WellFounded

WellFoundedSet

WellQuasiOrder

WithBot

Zorn

ZornAtoms

Probability

Distributions

Gaussian

HasGaussianLaw

Basic

Def

Independence

Basic

CharFun

Fernique

Multivariate

Real

Bernoulli

Fernique

Independence

Kernel

Indep

IndepFun

Basic

CharacteristicFunction

Integrable

Integration

Kernel

Composition

AbsolutelyContinuous

Comp

CompMap

CompNotation

CompProd

IntegralCompProd

KernelLemmas

Lemmas

MapComap

MeasureComp

MeasureCompProd

ParallelComp

Prod

RadonNikodym

WithDensity

Disintegration

Basic

CDFToKernel

CondCDF

Density

Integral

MeasurableStieltjes

StandardBorel

Unique

Basic

CondDistrib

Condexp

Defs

MeasurableIntegral

MeasurableLIntegral

RadonNikodym

WithDensity

Martingale

Basic

Convergence

Upcrossing

Moments

Basic

ComplexMGF

Covariance

CovarianceBilin

CovarianceBilinDual

IntegrableExpMul

MGFAnalytic

SubGaussian

Tilted

Variance

ProbabilityMassFunction

Basic

Constructions

Integrals

Monad

Process

Adapted

Filtration

HittingTime

Indistinguishable

LimitProcess

PartitionFiltration

Predictable

Stopping

ConditionalProbability

Density

HasLaw

IdentDistrib

Notation

UniformOn

RingTheory

AdicCompletion

Basic

Adjoin

Polynomial

Basic

Transcendental

Basic

Dimension

FG

Field

PowerBasis

Singleton

Tower

Algebraic

Basic

Defs

Integral

MvPolynomial

AlgebraicIndependent

Adjoin

AlgebraicClosure

Basic

Defs

TranscendenceBasis

Transcendental

Artinian

Defs

Module

Congruence

Basic

Defs

Opposite

Coprime

Basic

Ideal

Lemmas

DedekindDomain

Ideal

Basic

Lemmas

AdicValuation

Basic

Dvr

IntegralClosure

Derivation

Basic

DifferentialRing

MapCoeffs

DiscreteValuationRing

Basic

TFAE

Finiteness

Basic

Bilinear

Cardinality

Cofinite

Defs

Finsupp

Ideal

Lattice

Nakayama

Prod

Projective

Subalgebra

FractionalIdeal

Basic

Inverse

Operations

GradedAlgebra

Homogeneous

Ideal

Submodule

Basic

HahnSeries

Addition

Basic

Multiplication

PowerSeries

Summable

Ideal

MinimalPrime

Basic

Localization

Quotient

HasFiniteQuotients

Basic

Basic

Defs

Nilpotent

Noetherian

Operations

PowTransition

Basic

BigOperators

Colon

Cotangent

Defs

GoingUp

IsPrimary

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

KrullDimension

Basic

Zero

LocalProperties

Basic

IntegrallyClosed

Submodule

LocalRing

MaximalIdeal

Basic

Defs

ResidueField

Basic

Defs

Ideal

RingHom

Basic

Basic

Defs

Localization

AtPrime

Basic

Away

Basic

Algebra

AsSubring

BaseChange

Basic

Cardinality

Defs

FractionRing

Ideal

Integer

Integral

LocalizationLocalization

Module

NumDen

Submodule

MvPolynomial

MonomialOrder (file)

DegLex

Symmetric

Defs

Basic

Groebner

Homogeneous

Tower

WeightedHomogeneous

MvPowerSeries

Basic

Inverse

LexOrder

NoZeroDivisors

Order

Nilpotent

Basic

Defs

Lemmas

Noetherian

Basic

Defs

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Basic

Defs

Transitivity

OreLocalization

Basic

Cardinality

NonZeroDivisors

OreSet

Ring

Polynomial

Cyclotomic

Basic

Eval

Expand

Roots

Eisenstein

Basic

Criterion

Basic

Bernstein

Chebyshev

Content

DegreeLT

GaussLemma

Ideal

IntegralNormalization

Nilpotent

Pochhammer

Quotient

RationalRoot

ScaleRoots

SeparableDegree

Subring

Tower

UniqueFactorization

Vieta

PowerSeries

Basic

Inverse

NoZeroDivisors

Order

Trunc

Radical

Basic

RootsOfUnity

Basic

Complex

Minpoly

PrimitiveRoots

SimpleModule

Basic

SimpleRing

Basic

Defs

Matrix

Spectrum

Maximal

Basic

Defs

Localization

Prime

Basic

Defs

RingHom

Topology

TensorProduct

Basic

Finite

Free

Maps

MonoidAlgebra

MvPolynomial

Quotient

Trace

Basic

Defs

TwoSidedIdeal

Basic

Kernel

Lattice

Operations

UniqueFactorizationDomain

Basic

Defs

FactorSet

Finite

GCDMonoid

Ideal

Multiplicity

Nat

NormalizedFactors

Valuation

Discrete

Basic

ValuativeRel

Basic

Basic

ExtendToLocalization

Integers

IsTrivialOn

PrimeMultiplicity

ValuationRing

ValuationSubring

AdjoinRoot

AlgebraTower

Bezout

Binomial

ChainOfDivisors

EssentialFiniteness

EuclideanDomain

Filtration

FiniteLength

FinitePresentation

FiniteStability

FiniteType

FreeCommRing

FreeRing

IntegralDomain

IsPrimary

IsTensorProduct

LaurentSeries

Length

MatrixAlgebra

MatrixPolynomialAlgebra

Multiplicity

Nakayama

OrzechProperty

PolynomialAlgebra

PowerBasis

PrincipalIdealDomain

PrincipalIdealDomainOfPrime

ReesAlgebra

RingHomProperties

SurjectiveOnStalks

ZMod

SetTheory

Cardinal

Cofinality

Basic

Enum

Ordinal

Aleph

Arithmetic

Basic

Continuum

Defs

Divisibility

ENNReal

ENat

Finite

Finsupp

NatCard

Order

Ordinal

Pigeonhole

Rat

Regular

SchroederBernstein

Subfield

ToNat

Ordinal

Arithmetic

Basic

Enum

Exponential

Family

FixedPoint

FundamentalSequence

Principal

Univ

Tactic

Algebra

Basic

Lemmas

ArithMult (file)

Init

Attr

Core

Register

Basify

Attr

Bound (file)

Attribute

Init

CancelDenoms

Core

CategoryTheory

CategoryStar

Elementwise

IsoReassoc

Map

Reassoc

Slice

ClickSuggestions (file)

Apply

ApplyAt

FindPremises

GRewrite

Rewrite

SectionState

TryPremises

Unfold

Util

Continuity (file)

Init

FieldSimp (file)

Attr

Discharger

Lemmas

Finiteness (file)

Attr

FunProp (file)

Attr

Core

Decl

Elab

FunctionData

Mor

Theorems

ToBatteries

Types

GCongr (file)

Core

ForwardAttr

GRewrite (file)

Core

Elab

Linarith (file)

Oracle

SimplexAlgorithm (file)

Datatypes

Gauss

PositiveVector

SimplexAlgorithm

Datatypes

Frontend

Lemmas

Parsing

Preprocessing

Verification

LinearCombination (file)

Lemmas

Linter (file)

AuxLemma

DeclType

DeprecatedSyntaxLinter

DirectoryDependency

DocPrime

DocString

EmptyLine

FlexibleLinter

HashCommandLinter

HaveILetI

HaveLetLinter

Header

InternalConstructor

Lint

MinImports

Multigoal

OldObtain

OverlappingInstances

PPRoundtrip

PrivateModule

Style

TacticDocumentation

UnusedInstancesInType

UnusedTactic

UnusedTacticExtension

UpstreamableDecl

Whitespace

Measurability (file)

Init

Monotonicity

Attr

Nontriviality (file)

Core

NormNum (file)

Abs

Basic

BigOperators

Core

DivMod

Eq

GCD

Ineq

Inv

NatFactorial

OfScientific

Pow

Prime

Result

Order (file)

Graph

Basic

Tarjan

CollectFacts

Preprocessing

ToInt

Polynomial

Core

Positivity (file)

Basic

Core

Finset

Push (file)

Attr

Relation

Rfl

Ring (file)

Basic

Common

Compare

PNat

RingNF

Simproc

ExistsAndEq

Simps (file)

Basic

NotationClass

TacticAnalysis (file)

Declarations

Translate

Attributes

Core

Expr

GuessName

Reorder

TagUnfoldBoundary

ToAdditive

ToDual

UnfoldBoundary

Widget

Calc

CongrM

Conv

LibraryRewrite

SelectInsertParamsClass

SelectPanelUtils

Abel

AdaptationNote

Algebraize

ApplyAt

ApplyCongr

ApplyFun

ApplyWith

Basic

ByCases

ByContra

CasesM

Check

Choose

ClearExcept

ClearExclamation

Clear_

Coe

Common

ComputeDegree

CongrExclamation

CongrM

Constructor

ContinuousFunctionalCalculus

Contrapose

Conv

Convert

Core

CrossRefAttribute

DSimpPercent

DeclarationNames

DefEqAbuse

DefEqTransformations

DepRewrite

DeprecateTo

DeriveFintype

ENatToNat

Eqns

ErwQuestion

ExistsI

ExtendDoc

ExtractGoal

FBinop

FailIfNoProgress

FastInstance

Field

FinCases

Find

GrindAttrs

Group

GuardGoalNums

GuardHypNums

HaveI

HigherOrder

Hint

InferParam

Inhabit

IntervalCases

IrreducibleDef

Lemma

Lift

MinImports

MkIffOfInductiveProp

Module

ModuleNF

MoveAdd

NoncommRing

NthRewrite

Observe

OfNat

PPWithUniv

Peel

ProxyType

Qify

RSuffices

Recover

Rename

RenameBVar

Rify

Says

ScopedNS

Set

SetLike

SetNotationForOrder

Setm

SimpIntro

SimpRw

SplitIfs

Spread

Subsingleton

Substs

SuccessIfFailWithMsg

SudoSetOption

SuppressCompilation

SwapVar

TFAE

Tauto

TautoSet

TermCongr

ToAdditive

ToDual

ToExpr

ToFun

ToLevel

Trace

TryThis

TypeStar

UnsetOption

Use

Variable

WLOG

Zify

Topology

Algebra

Algebra (file)

Equiv

Group

Basic

ClosedSubgroup

Compact

ContinuousDiv

ContinuousInv

Defs

GroupTopology

Neighborhood

Order

Pointwise

Quotient

Subgroup

Torsor

Units

ZPow

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

Extend

Idempotent

Invertible

PiProd

Quotient

Restrict

RestrictScalars

Equiv

Basic

Pi

Prod

Multilinear

Basic

Bounded

Topology

Spaces

CharacterSpace

ContinuousLinearMap

UniformConvergenceCLM

WeakBilin

WeakDual

Basic

ClosedSubmodule

Complement

Determinant

FiniteDimension

LocallyConvex

ModuleTopology

PerfectPairing

PerfectSpace

Simple

Star

UniformConvergence

Monoid (file)

Defs

FunOnFinite

Nonarchimedean

Bases

Basic

Order

Archimedean

Field

Floor

Group

LiminfLimsup

Ring

Basic

Ideal

Real

SeparationQuotient

Basic

FiniteDimensional

Section

Star (file)

Real

ValuativeRel

Completion

ValuativeTopology

Valued

ValuationTopology

ValuedField

WithVal

Affine

AffineSubspace

ConstMulAction

Constructions

ContinuousAffineEquiv

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

LinearMapCompletion

LinearTopology

MulAction

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

StarSubalgebra

Support

UniformConvergence

UniformField

UniformFilterBasis

UniformMulAction

UniformRing

WithZeroTopology

Baire

CompleteMetrizable

Lemmas

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Real

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

Lattice

Ordered

Polynomial

Star

StarOrdered

StoneWeierstrass

Units

Weierstrass

Covering

AddCircle

Basic

Quotient

Defs

Basic

Filter

Induced

Sequences

Ultrafilter

EMetricSpace

Basic

BoundedVariation

Defs

Diam

Lipschitz

MulOpposite

Pi

VariationOnFromTo

FiberBundle

Basic

IsHomeomorphicTrivialBundle

Trivialization

GDelta

Basic

MetrizableSpace

Hom

ContinuousEval

ContinuousEvalConst

Homeomorph

Defs

Lemmas

Quotient

InductiveDimension

Classes

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

Defs

Dilation

DilationEquiv

Equicontinuity

Gluing

HausdorffDistance

IsometricSMul

Isometry

Lipschitz

Perfect

PiNat

Polish

ThickenedIndicator

Thickening

UniformConvergence

Metrizable

Basic

CompletelyMetrizable

Real

Uniformity

Urysohn

OpenPartialHomeomorph

Basic

Composition

Constructions

Continuity

Defs

IsImage

Order (file)

AtTopBotIxx

Basic

Bornology

Compact

DenselyOrdered

ExtendFrom

IntermediateValue

IsLUB

IsLocallyClosed

Lattice

LeftRight

LeftRightLim

LeftRightNhds

LiminfLimsup

LocalExtr

Monotone

MonotoneContinuity

MonotoneConvergence

OrderClosed

ProjIcc

Real

Rolle

T5

WithTop

PartialHomeomorph

Basic

Defs

Semicontinuity

Basic

Defs

Hemicontinuity

Lindelof

Separation

Basic

CountableSeparatingOn

GDelta

Hausdorff

Regular

SeparatedNhds

Sets

Closeds

Compacts

OpenCover

Opens

VietorisTopology

Spectral

Basic

Hom

Prespectral

UniformSpace

AbstractCompletion

Basic

Cauchy

Closeds

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

IndicatorConstPointwise

Inseparable

Irreducible

IsLocalHomeomorph

KrullDimension

LocalAtTarget

LocallyClosed

LocallyFinite

Neighborhoods

NhdsKer

NhdsSet

NhdsWithin

NoetherianSpace

Path

Perfect

Piecewise

QuasiSeparated

SeparatedMap

Sequences

Sion

Sober

Ultrafilter

UnitInterval

UrysohnsLemma

WithTopology

Util

AtomM (file)

Recurse

CodeActions (file)

BinderPlicity

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

MakeEditLink

OfRpcMethod

RefreshComponent

Data

Html (file)

Basic

Elab

Jsx

Cancellable

Compat

Util

Qq (file)

ForLean

Do

ReduceEval

ToExpr

AssertInstancesCommute

Commands

Delab

Macro

Match

MatchImpl

MetaM

Simp

SortLocalDecls

Typ

Std (file)

Data

DHashMap (file)

Internal

AssocList

Basic

Iterator

Lemmas

Defs

HashesTo

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDef

RawLemmas

DTreeMap

Internal

WF

Defs

Lemmas

Balanced

Balancing

Cell

Def

Lemmas

Model

Operations

Ordered

Queries

Raw

AdditionalOperations

Basic

Lemmas

WF

AdditionalOperations

Basic

Lemmas

ExtDHashMap (file)

Basic

Lemmas

ExtDTreeMap

Basic

Lemmas

ExtHashMap

Basic

Lemmas

ExtHashSet

Basic

Lemmas

ExtTreeMap

Basic

Lemmas

ExtTreeSet (file)

Basic

Lemmas

HashMap (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawLemmas

HashSet (file)

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

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

TreeMap

Raw

AdditionalOperations

Basic

Lemmas

WF

AdditionalOperations

Basic

Lemmas

TreeSet (file)

Raw

Basic

Lemmas

WF

AdditionalOperations

Basic

Lemmas

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

Internal (file)

ForIn

Basic

Order

Basic

PredTrans

Parsec (file)

Basic

ByteArray

String

Sat

AIG

Basic

LawfulOperator

LawfulVecOperator

RefVec

CNF

Basic

Literal

Sync

Basic

Mutex

Tactic

BVDecide (file)

Bitblast

BVExpr

Circuit

Impl

Operations

Mul

Do

ProofMode

Syntax

Time

Date (file)

Unit

Basic

Day

Month

Week

Weekday

Year

Basic

PlainDate

ValidDate

DateTime (file)

PlainDateTime

Timestamp

WallTime

Format (file)

Basic

DateFormat

Modifier

Internal (file)

Bounded

UnitVal

Notation

Spec

Time (file)

Unit

Basic

Hour

Millisecond

Minute

Nanosecond

Second

Basic

HourMarker

PlainTime

Zoned (file)

Database (file)

Basic

PosixTz

TZdb

TzIf

Windows

RecurringRule

TimeZone

ZoneRules

Duration

WP (file)

Monad (file)

Assertion

Basic

Tactic

references (file)

Color scheme

darksystemlight