General documentation

index

foundational types

tactics

Library

Open NN for TorchLean modules.↓

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

Lemmas

Merge

Scan

BinomialHeap

Basic

Fin

Basic

Fold

Lemmas

Float

Basic

List

Basic

Count

Lemmas

Pairwise

Perm

Scan

MLList

Basic

Nat

Bitwise (file)

Lemmas

Basic

Lemmas

Vector

Basic

Lemmas

ByteArray

UInt

Lean

Meta

Basic

DiscrTree

Expr

Inaccessible

InstantiateMVars

SavedState

UnusedNames

AttributeExtra

Except

Expr

HashSet

LawfulMonad

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

FloatLib

Floats (file)

ExecFloat (file)

Backends

Dispatch

Add

Proof

Runtime

Div

Proof

Runtime

Fma

Proof

Runtime

FmaWord

Proof

Runtime

Mul

Proof

Runtime

Sqrt

Proof

Runtime

SqrtWord

Proof

Runtime

FixedLimb

Pair

Addition

Proof

Runtime

Core

Proof

Runtime

Division

Proof

Runtime

Fma

Proof

Runtime

Multiplication

Proof

Runtime

Sqrt

Proof

Runtime

Subtraction

Proof

Runtime

Generic

AddDyadic

Proof

Runtime

Kernel

Proof

Runtime

ProductRound

Proof

Runtime

QuotientRound

Proof

ScaleAdd

Proof

Runtime

Sqrt

Proof

Runtime

Selection

Certified

Metadata

Policy

Report

Scoring

TinyTable

Generic

Certificates

Certified

Construction

Core

Indexing

Proof

Runtime

Table

WideLimb

Addition

Proof

Runtime

Core

Proof

Runtime

Finite

Proof

Fma

Proof

Runtime

Multiplication

Proof

Runtime

Round

Proof

Runtime

Word

Full

Addition

Proof

Runtime

Core

Proof

Runtime

Division

Proof

Runtime

Fma

Proof

Runtime

Sqrt

Proof

Runtime

Subtraction

Proof

Runtime

ModelSqrt

Proof

Runtime

Narrow

Addition

Proof

Runtime

Base

Proof

Runtime

Division

Proof

Runtime

Finite

Proof

Runtime

Fma

Proof

Runtime

Multiplication

Proof

Runtime

Rounding

Proof

Runtime

SignedMagnitude

Proof

Sqrt

Proof

Runtime

Agreement

DivisionReference

Packing

NormalPair

Proof

ProductRound

Proof

Runtime

Quotient

Proof

Small

Add

Proof

Runtime

Core

Proof

Runtime

Div

Proof

Runtime

Finite

Proof

Runtime

Mul

Proof

Runtime

TwoWordMul

Proof

Runtime

SqrtArithmetic

SqrtNormalRounding

Conversion

Core

Proof

Runtime

Core

Capability

Operations

Info (file)

Command

Inspection

Profile

Render

Proof

Arithmetic

Certificate

Spec

Arithmetic

Automation

Carrier

Comparison

Dispatch

ExactMap

Instances

Runtime

Formats (file)

BinaryInterchange (file)

Analysis

BFloat16

DyadicOrder

Error

Sterbenz

Arithmetic

LeanModel (file)

AddSub

SignedSemantics

Core

Subtraction

Constants

DivisionSemantics

Finite

FiniteSemantics

Finiteness

Proof

Runtime

Semantics

SqrtSemantics

Automation (file)

Finite

Complex

Automation

Core

Info

NumericalSystem

Semantics

Configured (file)

ByteTable

Proof

Runtime

Classification

Proof

Runtime

Comparison

Proof

Runtime

Conversion

Instances

Proof

Runtime

Core

Proof

Runtime

Interval (file)

Finite

Outward

Proof

Runtime

NativeFPU

Proof

Runtime

Operations

Proof

Runtime

Plan

Automatic

Candidates

Estimates

FirstOrder

Instances

NativeCandidates

WideLimbCandidates

Reduction (file)

Proof

Runtime

Tree

Rounding

Proof

Runtime

Storage

Code

Proof

Runtime

Family

Proof

Runtime

Codecs

Core

TotalOrder

Proof

Runtime

Value

Core

CoreProof

Formatting

Instances

NativeDispatch

Parsing

Transcendentals

Type

Conversion (file)

Cast

Proof

Runtime

Widening

Text

BoundedParsing

DecimalFormatting

DecimalFormattingProof

Formatting

Parsing

PrecisionProof

Representation

Roundtrip

Proof

Runtime

DType

Cast

Semantics

Descriptor

Plan

Candidates

Estimates

Instances

Routes

Backends

Carrier

Spec

DirectedSemantics

Dyadic

Core

Proof

Runtime

Packing

Rational

Packing

Branches

Downward

Grid

Internal

Upward

RoundingSemantics

Branches

Executable

Quotient

RoundedReal

Bounds

Conversion

Logarithm

NearestEven

Quotient

Runtime

Scaling

Addition

Basic

Bounds

Division

Exact

Finite

FiniteBounds

Internal

Multiplication

NonNaN

Positive

PositiveBounds

Power

Signed

SquareRoot

Subtraction

Dyadic

Classification

Core

Decode

Rational

Rounding

Format

Catalog

Definition

Properties

Runtime

Storage

Info

Command

Profile

Interval (file)

Activations

Arithmetic

Core

Info

IntervalSemantics (file)

Activations

Arithmetic

Core

Finite

MinMax

Order

Model

Fields

Optimized

Proof

Packing

Bounds

Finite

Special

Carrier

ERealSemantics

ExactNumericalSystem

ExactValue

Instances

Lean

NumericalSystem

RealSemantics

SignedERealSemantics

ModelRounding

Proof

Runtime

Operations

Adjacent

Proof

Boundaries

Core

Classification

Classes

Predicates

Proof

Runtime

Semantics

Compare

Predicates

Proof

Runtime

Proof

Runtime

MixedPrecision

Accumulation

Matmul

MatmulProof

Proof

Proof (file)

Exponent

InvalidSignals

Remainder

RoundToIntegral

TotalOrder

Encoding

ExactValue

Magnitude

Proof

Runtime

Semantics

Sign

Power

Runtime

Proof

Core

Exact

Finite

Reduction (file)

Proof

Runtime

Tree

RoundDyadicImpl

Proof

Runtime

Rounding

Accuracy

Model

Proof

Directed

Dyadic

Runtime

Policy

Agreement

Proof

Runtime

Mode

NearestEven

Proof

Spec

Division

Dyadic

SquareRoot

StaticByte (file)

Backend

Construction

Proof

Runtime

Conversion

Instances

Proof

Runtime

Core

Construction

Proof

Runtime

Plan

Construction

Proof

Runtime

Status (file)

Proof

Runtime

Transcendentals (file)

Config

Contract

ExpLog

FixedPoint

Hyperbolic

Trig

Semantics

Block (file)

Configured

Conversion

Instances

Proof

Runtime

Core

Info

Proof

Runtime

SharedScale

Core

Info

Proof

Runtime

Codebook (file)

Arithmetic

Proof

Runtime

Catalog

Proof

Runtime

Configured

Conversion

Proof

Runtime

Catalog

Core

Info

Proof

Runtime

Core

Nearest

Proof

Runtime

Automation

Info

DecimalInterchange (file)

Arithmetic

Basic

Operations

Proof

Runtime

Status

BID

Proof

Runtime

Codec

BitsProof

Proof

Runtime

Cohort

Optimal

Proof

Runtime

Comparison

Proof

Runtime

Conversion

Binary

FromProof

NearestAwayProof

Proof

Runtime

SpecialProof

ToProof

Format

Proof

Runtime

Integer

FromInt

Proof

Rounding

Runtime

Posit

Configured

Proof

Runtime

Proof

Runtime

DPD

Declet

DecletProof

FieldsProof

Proof

Runtime

Trailing

TrailingProof

Environment

Proof

Runtime

Formatting

Precision

PrecisionProof

Proof

Runtime

Words

Inspection

Basic

Runtime

Integral

Proof

Runtime

Neighbors

Adjacency

Endpoints

Grid

Proof

Runtime

Steps

Projection

Cohort

Direction

Exact

FormatProof

Minimal

Proof

Runtime

Scale

ScaleProof

Semantics

Zero

Quantize

Proof

Runtime

Queries

Proof

Runtime

Remainder

Integer

Proof

Runtime

Ties

Rounding

Proof

Runtime

Scaling

Proof

Runtime

Semantics

Sign

Proof

Runtime

Sqrt

Cohort

Direction

Exact

GridProof

Minimal

Proof

Runtime

ScaleProof

Semantics

TotalOrder

Proof

Runtime

Basic

Datum

DatumProof

Format

Interval

Runtime

FiniteOnly (file)

E4M3FNUZ

E5M2FNUZ

FixedPoint (file)

Bounded

Configured

Conversion

Instances

Proof

Runtime

Core

Info

Proof

Runtime

Semantics

Core

Proof

Automation

Core

Info

Configured

Conversion

Instances

Proof

Runtime

Core

Info

Instances

Plan

Proof

Runtime

Exact

Info

Proof

Runtime

Automation

Flocq (file)

Calculation

Arithmetic

Bracket

Operations

Round

Theory (file)

Analysis

Neighbors

StandardUlp

Sterbenz

SterbenzFLT

Ulp

Error

Addition

Bounds

Directed

DivisionSqrt

Exactness

Multiplication

Relative

Format

Digits

Formats

Generic

Magnitude

Theorems

Rounding

Affine

Away

Core

Double

Generic

Nearest

Odd

Order

Predicates

Properties

Scalar

NF

Representable

Special

FTZ

Arithmetic

Automation

Core

NumericalSystem

GenericFormat

IEEE754 (file)

Native (file)

Integer (file)

Constructors

FromInt

Rounding

ToInt

Model (file)

Representation

AddSub

Info

Representation

Sqrt

Logarithmic (file)

Configured

Conversion

Proof

Runtime

Core

Info

Instances

Plan

Proof

Runtime

Exact

Info

Proof

Runtime

Automation

OCP (file)

FP8

E4M3FN

E5M2

MX (file)

Configured

Conversion

Proof

Runtime

Core

Info

Proof

Runtime

E8M0

Automation

Block

Core

Info

Semantics

Standard

Configured

DotProduct

Proof

Runtime

Proof

Runtime

DotProduct

Proof

Runtime

Core

ElementProof

Proof

Runtime

ScaleProof

E2M1

E2M3

E3M2

P3109 (file)

Arithmetic

External

Bounds

Proof

Rounding

Runtime

Extrema

Proof

Runtime

Mixed

Proof

Runtime

Queries

Classification

Neighbors

Order

Proof

Runtime

Sqrt

Bounds

Proof

Runtime

Scaling

Selection

Instances

Proof

Runtime

Conversion

Comparison

Instances

Proof

Range

Runtime

Projection

Rational

Direction

Proof

Runtime

Selection

Semantics

Correctness

Direction

Encoding

Finite

Range

RealSelection

Rounding

Runtime

Selection

Info

Order

Proof

Runtime

Posit (file)

Algebraic

Power

Proof

Runtime

RationalPower

Proof

Runtime

Root

Proof

Runtime

Proof

Runtime

Arithmetic

Dyadic

Direct

Proof

Runtime

Proof

Runtime

Limb

Arithmetic

Proof

Runtime

Core

Proof

Runtime

Decode

Proof

Runtime

Packed

Add

Proof

Runtime

Boundary

Proof

Runtime

Fma

Proof

Runtime

Mul

Proof

Runtime

SignedSum

Proof

Runtime

Sqrt

Proof

Runtime

Sub

Proof

Runtime

Rounding

GuardSticky

Proof

Runtime

Proof

Runtime

Shared

GuardSticky

Proof

Runtime

Spec

Word

Arithmetic

Proof

Runtime

Core

Elimination

Proof

Runtime

Fields

Proof

Runtime

Primitive

Decode

Proof

Runtime

Fields

Proof

Runtime

Word

Proof

Runtime

Packed

Dyadic

Proof

Runtime

Product

Proof

Runtime

Quotient

Proof

Runtime

SignedSum

Proof

Runtime

SquareRoot

Proof

Runtime

Rounding

GuardSticky

DyadicTarget

Proof

Runtime

Semantics

Candidates

Interior

Spec

Fields

Midpoint

Stream

Tail

Layout

Proof

Runtime

WordLimb

Proof

Runtime

Spec

Cast

Integer

Unsigned

Proof

Runtime

Proof

Runtime

Widening

Configured (file)

Algebraic

RationalPower

Proof

Runtime

Proof

Runtime

Backend

FixedWords

Byte

Proof

Raw

Runtime

Word16

Proof

Raw

Runtime

Word32

Proof

Raw

Runtime

Word64

Proof

Raw

Runtime

Carrier

Common

Kernels

Proof

Runtime

ByteTable

Construction

Proof

Runtime

Conversion

Integer

Unsigned

Proof

Runtime

Proof

Runtime

Instances

Proof

Runtime

Elementary

Proof

Runtime

Functions

Basic

IntegerProof

Hyperbolic

Proof

Runtime

Logarithm

Proof

Runtime

Plan

ByteDispatch

Proof

Runtime

Core

Estimates

GeneralCandidates

ModelCandidates

ByteCandidates

Dispatch

Storage

Code

Proof

Runtime

Family

Proof

Runtime

Native

Core

Instances

Proof

Runtime

Pair

Proof

Runtime

Codecs

Core

Trigonometric

Atan2

Proof

Runtime

Pi

Proof

Runtime

Proof

Runtime

Value

Proof

Runtime

Comparison

Constants

Core

Instances

Interval

Projective

Real

Type

Elementary

Proof

Runtime

Formatting (file)

Configured

Proof

Runtime

Parsing

Proof

Functions

Basic

IntegerProof

Hyperbolic

Proof

Runtime

Logarithm

Proof

Runtime

Model

Basic

Decode

Fields

SignedMagnitude

Quire

Arithmetic

Proof

Runtime

Configured

Conversion

Proof

Runtime

Proof

Runtime

Type

Views

Model

Core

Proof

Semantics

Projective

Proof

Real

Runtime

Accumulation

Capacity

Info

Rounding

Comparison

Proof

Runtime

Direct

Candidate

Proof

Runtime

Proof

Runtime

Dyadic

Proof

Runtime

Enclosure

Convergence

Proof

Runtime

Prefix

Proof

Runtime

Quotient

Direct

Jamming

PrefixProof

Proof

Runtime

Semantics

Proof

Runtime

SquareRoot

Direct

PrefixProof

Proof

Runtime

Proof

Runtime

Proof

Real

RoundTrip

Runtime

Semantics

Exact

Proof

Runtime

Ordinary (file)

Real

Positive

BitRuns

Order

Trailing

OnePointOption

Projective

Real

Trigonometric

Atan2

Proof

Runtime

Pi

Proof

Runtime

Proof

Runtime

Comparison

Descriptor

Info

Interval

Interval (file)

ERealCoercions

Quantized

RealBounds

Rounders

Kernels (file)

FixedWord (file)

CertifiedDivision

Proof

Runtime

Core (file)

Proof (file)

Rounding

UInt128

Word

Runtime

Difference

Proof

Runtime

DyadicCompare

Proof

Runtime

IntegerSquareRoot

Proof

Runtime

LimbRound

Proof (file)

UInt128

UInt256

Runtime

Product

Proof

Runtime

Quotient

Compiler

Proof

Restoring128Proof

Runtime

RestoringSqrt

Compiler

Proof

Runtime

SignedMagnitude

UInt128

Proof

Proof

Runtime

LimbArray

Arithmetic

Proof

Runtime

Core

Proof

Runtime

Shift

Proof

Runtime

Numerics (file)

Automation

Attributes

Numerics

Capabilities (file)

BlockScaled

Elementary

Error

Ordered

Radix

Core (file)

Declaration

ExactSemantics

Proof

Representation

System

Value

Enclosure (file)

Comparison

Cache

Proof

Runtime

Elementary

ComplexTranscendental

Convergence

Irrational

Proof

Runtime

Termination

Transcendental

TrigonometricIrrational

Hyperbolic

Proof

Runtime

Interval

Basic

Bounds

Proof

Real

Runtime

Rational

AffineConvergence

Convergence

Proof

Runtime

Trigonometric

Pi

Convergence

Proof

Runtime

Termination

Reduction

Convergence

Proof

Runtime

Tangent

Runtime

AtanConvergence

AtanProof

Convergence

Proof

Runtime

SinCosConvergence

SinCosProof

Termination

Exact (file)

DecimalText

Notation

NotationProof

Precision

PrecisionProof

Proof

Runtime

Special

Dyadic

Arithmetic

Proof

Runtime

Comparison

Proof

Runtime

Basic

Format

Order

Real

Elementary

Proof

Runtime

HexText

Proof

Runtime

Hyperbolic

Proof

Runtime

RadixText

Precision

PrecisionProof

Runtime

ScannerProof

RationalPower

Enclosure

Proof

Runtime

Proof

Runtime

Trigonometric

Atan2

Enclosure

Proof

Runtime

Argument

Proof

Runtime

Pi

Proof

Runtime

PiValues

Inverse

Proof

Runtime

Tangent

TangentClassify

Proof

Runtime

RationalBinary

SignedRat

Zero

IEEEStatus (file)

Proof

Operation (file)

Proof (file)

Checked

Finite

Quantizer

Total

Context

Entropy

Semantics

Status

Order

Comparison

Quantization (file)

Affine (file)

Real

Deterministic (file)

ModularPower

Quotient

Rational

ShiftRight

Integer

Proof

Runtime

Automation

Directed

Ordered

Saturating

Spec

Stochastic

Reduction (file)

Error

Tree

Representations (file)

Boolean (file)

Arithmetic

Automation

FixedInt (file)

Semantics

Arithmetic

Basic

Refinement

Automation

Core

StaticStorage

ShiftRightJam (file)

Proof

Bitwise

IEEEClass

IEEEComparison

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

Float (file)

Model (file)

Format (file)

Basic

Valid

Unpacked (file)

Operations (file)

Add

Compare

Div

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

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

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

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

Float

Float32

IntToBitVec

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

IntToBitVec

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

Function

Hashable

LawfulHashable

NeZero

PLift

Prod

Queue

RArray

Random

Repr

Stream

ULift

Zero

Grind (file)

Homo (file)

BitVec

Fin

ISize

Int

Int16

Int32

Int64

Int8

List

Nat

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

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

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 (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

DeferredCheck

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)

Basic

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)

Conv (file)

Basic

Cbv

Change

Congr

Delta

Lets

Pattern

Rewrite

Simp

Unfold

Do (file)

Internal (file)

VCGen (file)

Context

Driver

EPost

Entails

FrameProc

FrameProcAttr

Frontend

LatticeOp

Reduce

RuleCache

RuleConstruction

Solve

SpecDB

Util

WPApp

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

ConjunctivePre

Contract

LetElim

Spec

Syntax

Grind (file)

Anchor

Annotated

BVDecide

Basic

BuiltinTactic

Cbv

Config

DSimp

DSimprocDSL

DSimprocDSLBuiltin

Filter

Have

Lint

LintExceptions

Main

Param

RegisterSymDSimp

RegisterSymSimp

Rewrite

ShowState

SimprocDSL

SimprocDSLBuiltin

Sym

Trace

WithGrindTacticM

Omega (file)

Core

Frontend

MinNatAbs

OmegaM

AsAuxLemma

AutoTry

BVDecide

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)

CodeQuality (file)

Basic

Frontend

EnvLinter (file)

Basic

Frontend

Extra (file)

DupNamespace

UnnecessarySeqFocus

UnreachableTactic

UnusedDecidableInType

AmbiguousOpen

Basic

Builtin

CheckUnivs

Coe

ConstructorAsVariable

CoreInternal

DefProp

Deprecated

DocsOnAlt

GlobalAttributeIn

Init

InternalModule

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

CollectHyps

EmbeddedConstraint

Enums

IntToBitVec

Reduction

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

BitVec

Cases

CasesMatch

CastLike

CheckResult

CollectParams

Core

Ctor

CtorIdx

Diseq

EMatch

EMatchAction

EMatchTheorem

EMatchTheoremParam

EMatchTheoremPtr

EqResolution

Ext

ExtAttr

Extension

Filter

Finish

ForallProp

Homo

Injection

Injective

Internalize

Intro

Inv

LawfulEqCmp

Lookahead

MBTC

Main

MarkAccessible

MarkNestedSubsingletons

MatchCond

MatchDiscrOnly

OrderInsts

PP

Parser

Proj

Proof

ProofUtil

Propagate

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

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

PostprocessTraces (file)

Basic

PostprocessTracesCommand

Postprocessors

StoredTraces

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

Mathlib

Algebra

Algebra

Spectrum

Basic

Pi

Quasispectrum

Subalgebra

Basic

Directed

IsSimpleOrder

Lattice

Operations

Prod

Tower

Basic

Bilinear

Defs

Equiv

Hom

IsSimpleRing

NonUnitalHom

NonUnitalSubalgebra

Operations

Opposite

Pi

Prod

Rat

RestrictScalars

StrictPositivity

Tower

TransferInstance

Unitization

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

Central

Basic

Defs

CharP

Algebra

Basic

Defs

Frobenius

Invertible

Lemmas

Reduced

Two

CharZero

Defs

Infinite

Quotient

DirectSum

Basic

Decomposition

Finsupp

Module

Divisibility

Basic

Hom

Units

EuclideanDomain

Basic

Defs

Field

Int

Exact

Basic

Field

Subfield

Basic

Defs

Basic

Defs

Equiv

GeomSum

IsField

NegOnePow

Opposite

Periodic

Rat

FiniteSupport

Basic

Defs

FreeAbelianGroup

Finsupp

FreeMonoid

Basic

UniqueProds

GCDMonoid

Basic

Finset

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

Graph

Idempotent

Indicator

InjSurj

IsCommutative

ModEq

Monoid

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

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

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

Field

Free

Pi

Basic

BigOperators

Defs

End

Hom

MinimalAxioms

NatInt

Opposite

PUnit

Pi

Prod

Projective

Rat

RingHom

Shrink

SpanRank

TransferInstance

ULift

MonoidAlgebra

Basic

Defs

Degree

Division

Lift

MapDomain

Module

NoZeroDivisors

Opposite

Support

MvPolynomial

Basic

Degrees

Derivation

Equiv

Eval

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

Defs

DenselyOrdered

Finset

Indicator

Int

Lattice

MinMax

Multiset

Nat

Opposite

OrderIso

PiLex

PosPart

Synonym

Units

GroupWithZero

Action

Synonym

Basic

Canonical

Defs

Finset

OrderIso

Submonoid

Synonym

Hom

Basic

Monoid

MonoidWithZero

Ring

TypeTags

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

GeomSum

InjSurj

Int

Interval

NNRat

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

Pointwise

Stabilizer

Polynomial

Degree

Defs

Domain

Lemmas

Monomial

Operations

SmallDegree

Support

TrailingDegree

Units

Eval

Algebra

Coeff

Defs

Degree

SMul

Subring

Module

AEval

Basic

AlgebraMap

Basic

BigOperators

CancelLeads

Coeff

Derivative

Div

EraseLead

Expand

FieldDivision

GroupRingAction

HasseDeriv

Identities

Inductions

Laurent

Lifts

Monic

Monomial

Reverse

RingDivision

Roots

Splits

SumIteratedDerivative

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

Units

Subsemiring

Basic

Defs

AddAut

Associated

Aut

Basic

Center

Centralizer

CharZero

Commute

CompTypeclasses

Defs

Equiv

Fin

GeomSum

GrindInstances

Idempotent

InjSurj

Invertible

Nat

NegOnePow

NonZeroDivisors

Opposite

PUnit

Parity

Periodic

Pi

Prod

Rat

Regular

Semiconj

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

FreeAlgebra

IsPrimePow

NeZero

Opposites

QuadraticDiscriminant

Quotient

Analysis

Analytic

Basic

CPolynomial

CPolynomialDef

ChangeOrigin

Composition

Constructions

ConvergenceRadius

Inverse

IsolatedZeros

IteratedFDeriv

Linear

OfScalars

Uniqueness

Within

Asymptotics

Arith

AsymptoticEquivalent

Basic

Defs

Lemmas

Prod

Ring

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

CPolynomial

Comp

Defs

Deriv

FTaylorSeries

FaaDiBruno

Operations

RCLike

WithLp

Deriv

Abs

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

Symmetric

WithLp

Gradient

Basic

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

Asymptotics

Basic

CauchyIntegral

Circle

Convex

Exponential

IsIntegral

Norm

Order

ReImTopology

RealDeriv

Spectrum

Trigonometric

Convex

Cone

Extension

SpecificFunctions

Basic

Deriv

Basic

Combination

Deriv

EGauge

Function

Gauge

Hull

Jensen

Mul

PathConnected

Segment

Slope

Star

StdSimplex

Strict

Strong

Topology

Fourier

BoundedContinuousFunctionChar

FourierTransform

Notation

InnerProductSpace

Projection

Basic

FiniteDimensional

Minimal

Reflection

Submodule

Adjoint

Basic

Calculus

Continuous

Defs

Dual

GramMatrix

GramSchmidtOrtho

LinearMap

Orientation

Orthogonal

Orthonormal

PiL2

Positive

ProdL2

Rayleigh

Spectrum

Subspace

Symmetric

LocallyConvex

BalancedCoreHull

Basic

Bounded

ContinuousOfBounded

HahnBanach

SeparatingDual

Separation

WeakDual

WithSeminorms

Matrix

Hermitian

HermitianFunctionalCalculus

MeasurableSpace

Normed

Order

PosDef

Spectrum

Normed

Affine

AddTorsor

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

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

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

RCLike

Basic

BoundedContinuous

Extend

Lemmas

Sqrt

Real

Pi

Bounds

Cardinality

Spectrum

Sqrt

SpecialFunctions

Complex

Analytic

Arctan

Arg

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

ERealExp

InvLog

NegMulLog

Pow

Asymptotics

Complex

Continuity

Deriv

NNReal

Real

Trigonometric

Angle

Arctan

ArctanDeriv

Basic

Bounds

Complex

ComplexDeriv

Deriv

DerivHyp

Inverse

Sinc

Arcosh

Arsinh

Artanh

Bernstein

Exp

ExpDeriv

Exponential

ImproperIntegrals

JapaneseBracket

MulExpNegMulSq

MulExpNegMulSqIntegral

NonIntegrable

PolarCoord

Sigmoid

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

IsEmpty

Basic

Defs

Logic

Basic

NNReal

Basic

Defs

Star

Nontrivial

Basic

Defs

Real

Basic

ConjExponents

ENatENNReal

Pointwise

Star

Rel (file)

Cover

Separated

Sign

Basic

Defs

Denumerable

ExistsUnique

Nonempty

Unique

UnivLE

Combinatorics

Enumerative

Partition

Basic

Composition

InclusionExclusion

Stirling

Control

Monad

Basic

Traversable

Basic

Applicative

Basic

Bifunctor

Combinators

EquivFunctor

Functor

ULift

Data

Bool

Basic

Set

DFinsupp

BigOperators

Defs

Ext

Lex

Module

NeLocus

Order

Sigma

Submonoid

ENat

Basic

Defs

Lattice

Monoid

Pow

SuccOrder

EReal

Basic

Inv

Operations

Fin

Tuple

Basic

Embedding

NatAntidiagonal

Reflection

Sort

Basic

Embedding

Rev

SuccPred

VecNotation

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

NAry

NatAntidiagonal

NoncommProd

Option

Order

Pairwise

Pi

Piecewise

Powerset

Preimage

Prod

Range

SDiff

Sigma

Sort

Sum

Sym

SymmDiff

Union

Update

Finsupp

Antidiagonal

Basic

Defs

Ext

Fin

Fintype

Indicator

Lex

Multiset

Option

Order

SMul

SMulWithZero

Single

ToDFinsupp

Weight

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

Basic

Embedding

Equiv

Group

IsApply

Module

Ring

Int

Cast

Basic

Defs

Field

Lemmas

Pi

Prod

Order

Basic

Units

Basic

CharZero

ConditionallyCompleteOrder

DivMod

GCD

Init

Interval

LeastGreatest

Log

ModEq

NatAbs

Notation

Sqrt

SuccPred

List

Perm

Basic

Lattice

Subperm

Basic

Chain

Count

Cycle

Dedup

Defs

Duplicate

Enum

FinRange

Find

Flatten

Fold

Forall2

GetD

Induction

Infix

InsertIdx

Iterate

Lattice

Lex

MinMax

Monad

NatAntidiagonal

Nodup

NodupEquivFin

OfFn

OffDiag

Pairwise

Permutation

Pi

Prime

ProdSigma

Range

Rotate

Sort

Sublists

Sym

TFAE

TakeDrop

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

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

DoubleFactorial

Factorization

Basic

Defs

Induction

LCM

GCD

Basic

BigOperators

NthRoot

Defs

Order

Lemmas

Prime

Basic

Defs

Factorial

Infinite

Int

Pow

Basic

BinaryRec

Bits

Bitwise

Count

Factors

Find

Init

Log

MaxPowDiv

ModEq

Multiplicity

Notation

PadicValNat

Pairing

Periodic

PrimeFin

Set

Sqrt

SuccPred

Totient

WithBot

Option

Basic

Defs

NAry

Ordering

Basic

PNat

Basic

Defs

Equiv

Notation

Prod

Basic

Lex

PProd

TProd

Rat

Cast

CharZero

Defs

Lemmas

Order

BigOperators

Defs

Encodable

Floor

Init

Lemmas

Sqrt

Set

Finite

Basic

Lattice

Lemmas

Powerset

Range

Lattice

Bounded

Disjoint

Image

Indexed

Order

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

Prod

Restrict

Semiring

Sigma

Subset

Subsingleton

SymmDiff

UnionLift

SetLike

Basic

Setoid

Partition (file)

Card

Basic

Sigma

Basic

Lex

String

Defs

Sum

Basic

Order

Sym

Sym2 (file)

Init

Basic

Tree

Basic

Vector

Basic

Defs

W

Basic

Cardinal

ZMod

Aut

Basic

Defs

IntUnitsPower

QuotientGroup

BitVec

Bracket

FinEnum

Ineq

Part

Quot

SProd

Subtype

ULift

Dynamics

Ergodic

MeasurePreserving

FixedPoints

Basic

Defs

Topology

PeriodicPts

Defs

Lemmas

Minimal

FieldTheory

Galois

Notation

IntermediateField

Adjoin

Algebra

Basic

Defs

Algebraic

Basic

IsAlgClosed

Basic

Spectrum

Minpoly

Basic

Field

Normal

Defs

SplittingField

Construction

IsSplittingField

Extension

Finiteness

Fixed

KummerPolynomial

Perfect

Separable

Tower

Geometry

Convex

Cone

Basic

Pointed

ConvexSpace

AffineMap

Barycenter

CompactSpaceStdSimplex

Defs

Module

ModuleTopology

PathConnectedSpaceStdSimplex

Prod

Topology

Set

Star

GroupTheory

Abelianization

Defs

Commutator

Basic

Congruence

Basic

BigOperators

Defs

Hom

Opposite

Coset

Basic

Card

Defs

FreeGroup

Basic

GroupAction

DomAct

Basic

SubMulAction (file)

OfFixingSubgroup

OfStabilizer

Pointwise

Basic

Blocks

ConjAct

Defs

Embedding

FixedPoints

FixingSubgroup

Hom

IterateAct

MultipleTransitivity

Pointwise

Primitive

Quotient

Ring

Transitive

MonoidLocalization

Away

Basic

Divisibility

Maps

MonoidWithZero

OreLocalization

Basic

OreSet

Perm

Cycle

Basic

Factors

Type

Basic

Closure

ConjAct

Fin

Finite

List

Option

Sign

Support

QuotientGroup

Basic

Defs

Finite

ModEq

SpecificGroups

Cyclic (file)

Basic

Alternating

Subgroup

Center

Centralizer

Simple

Submonoid

Center

Centralizer

Subsemigroup

Center

Centralizer

Archimedean

Complement

DedekindFinite

Divisible

Exponent

Finiteness

FreeAbelianGroup

Index

IndexNormal

NoncommPiCoprod

OrderOfElement

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

AffineEquiv

AffineMap

Basis

Centroid

Combination

Defs

Independent

Midpoint

Ordered

Pointwise

Restrict

Slope

Alternating

Basic

Basis

Basic

Bilinear

Cardinality

Defs

Fin

Prod

SMul

Submodule

VectorSpace

BilinearForm

Basic

Hom

Properties

Charpoly

BaseChange

Basic

ToMatrix

Complex

Module

Dimension

Basic

Constructions

DivisionRing

ErdosKaplansky

Finite

Finrank

Free

FreeAndStrongRankCondition

LinearMap

Localization

OrzechProperty

RankNullity

StrongRankCondition

Subsingleton

DirectSum

Finsupp

TensorProduct

Dual

BaseChange

Basis

Defs

Lemmas

Eigenspace

Basic

Charpoly

ContinuousLinearMap

Matrix

Minpoly

FiniteDimensional

Basic

Defs

Lemmas

Finsupp

Defs

LSum

LinearCombination

Pi

Span

SumProd

Supported

VectorSpace

FreeModule

Finite

Basic

Matrix

Basic

StrongRankCondition

GeneralLinearGroup

AlgEquiv

Basic

LinearIndependent

Algebra

Basic

Defs

Lemmas

Matrix

Charpoly

Basic

Coeff

Disc

Eigs

LinearMap

Determinant

Basic

GeneralLinearGroup

Basic

Defs

FinTwo

Projective

Action

Adjugate

Basis

BilinearForm

Block

ConjTranspose

Defs

Diagonal

DotProduct

Dual

Hadamard

Hermitian

Ideal

InvariantBasisNumber

Invertible

Kronecker

MvPolynomial

Nondegenerate

NonsingularInverse

Notation

Polynomial

PosDef

ProjectiveSpecialLinearGroup

Rank

Reindex

RowCol

SchurComplement

SemiringInverse

SesquilinearForm

SpecialLinearGroup

StdBasis

Symmetric

ToLin

ToLinearEquiv

Trace

Transvection

Vec

ZPow

Multilinear

Basic

Basis

Curry

DFinsupp

Finsupp

Projectivization

Action

Basic

QuadraticForm

Basic

Quotient

Basic

Card

Defs

SModEq

Basic

SesquilinearForm

Basic

Orthogonal

Span

Basic

Defs

TensorProduct

Associator

Basic

Basis

Defs

Finiteness

Map

Pi

Prod

Quotient

RightExactness

Tower

Transvection

Basic

BilinearMap

Center

Contraction

DFinsupp

Determinant

FixedSubmodule

InvariantBasisNumber

Isomorphisms

LinearPMap

Orientation

Pi

Prod

Projection

Ray

SpecialLinearGroup

StdBasis

Trace

UnitaryGroup

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

Defs

DependsOn

Iterate

ULift

Small

Basic

Defs

List

Set

OpClass

Pairwise

Relation

Relator

MeasureTheory

Constructions

BorelSpace

Basic

Complex

ContinuousLinearMap

Metric

Metrizable

Order

Real

Polish

Basic

EmbeddingReal

StronglyMeasurable

Pi

Covering

Besicovitch

BesicovitchVectorSpace

DensityTheorem

Differentiation

OneDim

Vitali

VitaliFamily

Function

ConditionalExpectation

AEMeasurable

Basic

CondexpL1

CondexpL2

Unique

L1Space

AEEqFun

HasFiniteIntegral

Integrable

LpSeminorm

Basic

ChebyshevMarkov

CompareExp

Defs

Indicator

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

ConvergenceInMeasure

Egorov

EssSup

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

Prod

Measure

CharacteristicFunction

Basic

Decomposition

Exhaustion

Hahn

Lebesgue

RadonNikodym

Dirac

Basic

Def

Haar

Basic

InnerProductSpace

NormedSpace

OfBasis

Quotient

Unique

Lebesgue

Basic

Complex

EqHaar

Integral

Typeclasses

Finite

NullSingletonClass

Probability

SFinite

AEDisjoint

AEMeasurable

AbsolutelyContinuous

Basic

Comap

CompleteLattice

Content

Continuity

Count

Doubling

EverywherePos

Filter

FiniteMeasure

FiniteMeasureExt

FiniteMeasurePi

GiryMonad

HasOuterApproxClosed

Interval

LevyProkhorovMetric

Map

MeasureSpaceDef

Module

MutuallySingular

NullMeasurable

OpenPos

OuterMeasure

Portmanteau

ProbabilityMeasure

Prod

QuasiMeasurePreserving

Real

Regular

RegularityCompacts

Restrict

Stieltjes

Sub

Sum

Tight

Trim

WithDensity

Order

Lattice

OuterMeasure

AE

Basic

BorelCantelli

Caratheodory

Defs

Induced

OfFunction

Operations

SpecificCodomains

Pi

WithLp

PiSystem

Topology

NumberTheory

Padics

PadicVal

Defs

Real

Irrational

Transcendental

Lindemann

AnalyticalPart

Zsqrtd

Basic

GaussianInt

Divisors

Niven

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

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

Basic

Bounded

BoundedLattice

CompleteLattice

Lattice

Lex

Order

Set

WithTopBot

Interval

Finset

Basic

Defs

Fin

Gaps

Nat

SuccPred

Set

Basic

Defs

Disjoint

Fin

Image

Infinite

IsoIoo

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

RelIso

Basic

Set

SuccPred

Archimedean

Basic

CompleteLinearOrder

InitialSeg

IntervalSucc

Limit

LinearLocallyFinite

Relation

WithBot

UpperLower

Basic

Closure

CompleteLattice

Fibration

Principal

Antichain

Antisymmetrization

Basic

BourbakiWitt

Circular

Closure

Cofinal

Compare

CompleteBooleanAlgebra

CompleteLatticeIntervals

Copy

Cover

DirSupClosed

Directed

Disjoint

Disjointed

FixedPoints

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

SetNotation

Shrink

Sublattice

SupClosed

SupIndep

SymmDiff

TypeTags

ULift

WellFounded

WellFoundedSet

WellQuasiOrder

WithBot

Zorn

ZornAtoms

Probability

Distributions

Gaussian

Basic

CharFun

Fernique

Multivariate

Real

Fernique

Independence

Kernel

Indep

IndepFun

Basic

Integrable

Integration

Kernel

Composition

Comp

CompMap

CompNotation

CompProd

KernelLemmas

MapComap

MeasureComp

MeasureCompProd

ParallelComp

Prod

Basic

Defs

MeasurableLIntegral

Moments

Basic

ComplexMGF

Covariance

CovarianceBilin

CovarianceBilinDual

IntegrableExpMul

MGFAnalytic

Variance

ConditionalProbability

Density

HasLaw

IdentDistrib

Notation

UniformOn

RingTheory

Adjoin

Polynomial

Basic

Basic

Dimension

FG

Field

Singleton

Tower

Algebraic

Basic

Defs

Integral

Congruence

Basic

Defs

Opposite

Coprime

Basic

Lemmas

Derivation

Basic

Finiteness

Basic

Bilinear

Cardinality

Cofinite

Defs

Finsupp

Ideal

Lattice

Prod

Projective

Subalgebra

Ideal

MinimalPrime

Basic

Quotient

Basic

Defs

Nilpotent

Noetherian

Operations

Basic

BigOperators

Colon

Defs

IsPrimary

Lattice

Maps

Maximal

Nonunits

Operations

Over

Pointwise

Prime

Prod

Span

Int

Basic

IntegralClosure

Algebra

Basic

Defs

IsIntegral

Basic

Defs

IsIntegralClosure

Basic

Defs

IntegrallyClosed

Jacobson

Ideal

Radical

LocalRing

MaximalIdeal

Basic

Defs

Basic

Defs

Localization

AtPrime

Basic

Away

Basic

Algebra

BaseChange

Basic

Defs

FractionRing

Ideal

Integer

Integral

LocalizationLocalization

Module

NumDen

MvPolynomial

Symmetric

Defs

Tower

Nilpotent

Basic

Defs

Lemmas

Noetherian

Basic

Defs

Orzech

UniqueFactorizationDomain

NonUnitalSubring

Basic

Defs

NonUnitalSubsemiring

Basic

Defs

Norm

Defs

OreLocalization

Basic

NonZeroDivisors

OreSet

Ring

Polynomial

Resultant

Basic

Basic

Bernstein

Content

DegreeLT

Ideal

IntegralNormalization

Nilpotent

Pochhammer

Quotient

RationalRoot

ScaleRoots

Subring

Tower

UniqueFactorization

Vieta

Radical

Basic

RootsOfUnity

Basic

Complex

PrimitiveRoots

SimpleModule

Basic

SimpleRing

Basic

Defs

Matrix

Spectrum

Maximal

Defs

Prime

Defs

TensorProduct

Basic

Finite

Free

IsBaseChangeFree

IsBaseChangeHom

IsBaseChangePi

Maps

MonoidAlgebra

MvPolynomial

Quotient

TwoSidedIdeal

Basic

Kernel

Lattice

Operations

UniqueFactorizationDomain

Basic

Defs

FactorSet

Finite

GCDMonoid

Ideal

Multiplicity

NormalizedFactors

AdjoinRoot

AlgebraTower

EssentialFiniteness

EuclideanDomain

FinitePresentation

FiniteType

IntegralDomain

IsPrimary

IsTensorProduct

MatrixAlgebra

MatrixPolynomialAlgebra

Multiplicity

OrzechProperty

PolynomialAlgebra

PowerBasis

PrincipalIdealDomain

SetTheory

Cardinal

Cofinality

Basic

Enum

Ordinal

Aleph

Arithmetic

Basic

Continuum

Defs

ENNReal

ENat

Embedding

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

Attr

Core

Register

Bound (file)

Attribute

Init

CancelDenoms

Core

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

DeprecatedSyntaxLinter

DirectoryDependency

DocPrime

DocString

EmptyLine

FlexibleLinter

GlobalAttributeIn

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

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

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

Eqns

ErwQuestion

ExistsI

Ext

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

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

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

Multilinear

Basic

Bounded

Topology

Spaces

CharacterSpace

ContinuousLinearMap

UniformConvergenceCLM

WeakBilin

WeakDual

Basic

ClosedSubmodule

Complement

Determinant

Equiv

FiniteDimension

LocallyConvex

ModuleTopology

PerfectPairing

PerfectSpace

Simple

Star

UniformConvergence

Monoid (file)

Defs

FunOnFinite

Order

Archimedean

Field

Floor

Group

LiminfLimsup

Ring

Basic

Ideal

Real

SeparationQuotient

Basic

FiniteDimensional

Section

Star (file)

Real

Affine

AffineSubspace

ConstMulAction

Constructions

ContinuousAffineEquiv

ContinuousAffineMap

ContinuousMonoidHom

Equicontinuity

Field

FilterBasis

GroupCompletion

GroupWithZero

Indicator

LinearMapCompletion

MulAction

NonUnitalAlgebra

NonUnitalStarAlgebra

OpenSubgroup

Polynomial

StarSubalgebra

Support

UniformConvergence

UniformField

UniformMulAction

UniformRing

Baire

CompleteMetrizable

Lemmas

Bornology

Absorbs

Basic

BoundedOperation

Constructions

Hom

Real

Compactification

OnePoint

Basic

ProjectiveLine

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

Defs

Basic

Filter

Induced

Sequences

Ultrafilter

EMetricSpace

Basic

BoundedVariation

Defs

Diam

Lipschitz

MulOpposite

Pi

VariationOnFromTo

FiberBundle

IsHomeomorphicTrivialBundle

GDelta

Basic

MetrizableSpace

Hom

ContinuousEval

ContinuousEvalConst

Homeomorph

Defs

Lemmas

Quotient

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

Urysohn

OpenPartialHomeomorph

Basic

Composition

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

Basic

Defs

Semicontinuity

Basic

Defs

Hemicontinuity

Separation

Basic

CountableSeparatingOn

GDelta

Hausdorff

Regular

SeparatedNhds

Sets

Closeds

Compacts

Opens

VietorisTopology

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

Continuous

ContinuousOn

DenseEmbedding

DiscreteSubset

ExtendFrom

IndicatorConstPointwise

Inseparable

Irreducible

LocallyClosed

LocallyFinite

Neighborhoods

NhdsKer

NhdsSet

NhdsWithin

NoetherianSpace

Path

Perfect

Piecewise

QuasiSeparated

Sequences

TietzeExtension

Ultrafilter

UnitInterval

UrysohnsBounded

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

NN (file)

API (file)

Autograd (file)

Complex

Differential

Function

Model

CLI (file)

Training (file)

Command

Command

Parser

Trainer

TrainingFlags

Data (file)

Image

Loaders

Sources

Synthetic

Text

Training

Models (file)

CausalTransformer (file)

Architecture

Runtime

Diffusion (file)

Sampling

Cnn

FNO

Generative

KAN

Mamba

PPO

Recurrent

ResNet

SelfSupervised

Unet

Vit

Module (file)

Command

Execution

Neural (file)

Layers (file)

Attention

Convolution

Pooling

Blocks

Builders

Execution

Impl

Indexed

Leading

Positional

State

Summary

Training

Transformer

Optim (file)

Config

RL (file)

Cli

Core

Runtime

SelfSupervised (file)

BlockMask

Text (file)

Bpe

Generation

Options

Tokenizer

Unicode

Vocabulary

Trainer (file)

Train (file)

Loop

Constructor

Core

Dataset

FixedSample

Memory

Reporting

Results

Run

Runner

Scheduler

Session

Summary

Verification (file)

Core

Execution

Lowering

Adapters

Arguments

Arithmetic

Checkpoint

Init

Json

Loss

Macros

Precision

Rand

Runtime

Sample

Seeded

Backend (file)

Attention

Audit

Availability

Capsule

ContractCheck

Grouping

IR

LibTorch

NativeCUDA

Planner

Profile

Reference

Registry

Report

Types

CI

SlowProofs

Core

Numeric (file)

Angle (file)

Real

Quotient

Real

ExternalProcess

Data

IO (file)

Csv

Npy

Parsing

SampleStream

Examples (file)

BugZoo

All

AttentionMask

AutogradDomain

BatchInvariance

CompilerBoundary

ConstantNormalizationSlice

FloatBoundary

Geometry3DProjection

IgnoredLabelLoss

KVCache

LayerNormDegenerateAxis

NormalizationState

RoPEPosition

ShapeAndBroadcast

StableLoss

TokenizerBoundary

Data

Loaders (file)

Cifar10Images

Csv

Npy

RealPaths

SamplePaths

DeepDives (file)

Floats

ArbIEEEExecCompare

EffectiveRounding

Float32Semantics

GraphNumericalCertificate

GraphSpec

Tutorial

AutogradTransforms

IRAxisOps

OneSemanticUniverse

TensorOperations

TorchIRPyTorch

Widgets

Factorization (file)

Check

Cholesky

Common

QR

Functional

Transcendentals

Interop

PyTorch (file)

Roundtrip

Models (file)

Common (file)

RealData

Train

Generative (file)

Autoencoder

Diffusion

Mae

Operators (file)

ComplexRegression

Fno1dBurgers

Pinn

RL (file)

Views (file)

GymnasiumRollout

PPOCartPole

PPOGridWorld

PPOPongRam

DQNReplay

PPOCartPole

PPOGridWorld

PPOPongRam

Sequence (file)

CharGpt

Gpt2

Gpt2Saved

GptAdder

Lstm

Mamba

Rnn

TextGpt2

Transformer

Supervised (file)

Kan

LstmRegression

Mlp

Vision (file)

Cnn

ResNet

Vit

Optimization (file)

MuonCertificates

Quickstart (file)

AutogradBasics

Common

Precision

Proofs

SimpleMlpTrain

TensorBasics

TypedTraining

Widgets

Support (file)

Command

Training

Runner

Verification

Floats (file)

Arb (file)

Oracle

FP32 (file)

Core

Error

Notation

Sterbenz

IEEEExec

Bridge

Finite

Interval (file)

Comparison

FP32

IEEEExec32

IEEEExec32ArbTrans

Quantization

GraphSpec (file)

Chain

ToDAG (file)

Core

Model

Semantics

Lowering

Primitives

Semantics

Syntax

DAG (file)

Primitives

Core

LinearAlgebra

Nonlinear

Normalization

Shape

Core

Lowering

Model

Semantics

Syntax

Term

Models (file)

Cnn

Mlp

MlpDeterministicInit

MlpSpecEquivalence

ResidualLinear

Primitives (file)

Embedding

Spatial

Core

ToSequential

IR (file)

Check

Graph

HardMask

Infer

OpContracts

Operator

Payload

Pretty

Semantics

ShapeSoundness

MLTheory (file)

CROWN

BoundOps (file)

Lawful

Cert

AlphaBetaCROWN

AlphaCROWN

Extras

AlphaConfig

BoundOpsIEEE32Exec

FP32

IntervalLemmas

Graph (file)

Engine (file)

CROWN

Activations

Linear

Node

Run

Structural

Affine

BackwardObjective

Base

Derivatives

Enclosure

IBP

Refinement

Core

Theorems

Lyapunov

TwoStage

Core

Execution

LossAnalysis

PipelineIIHybrid

PipelineIIIAllInLean

PipelineIPythonOnly

Certificate

Verification

Models

Mlp

Operators (file)

Activations

Arithmetic

BatchNorm

Conv

Slice

Proofs

GraphAlphaCrownTransferSoundness (file)

Alpha (file)

Basic

Fallback

Leaf

Linear

ReLU

Shape

AlphaBeta (file)

ReLUPhase

StepInversion

Common

EndToEnd

GraphCertSoundness (file)

Main (file)

AffineOps

ArithOps

Extraction

LeafOps

Softplus

UnaryOps

CertificateStep

IntervalLemmas

NonlinearOps

Semantics

Softplus

AlphaBetaReLUScalarSoundness

AlphaReLULowerBound

Distillation

GraphCrownCertSoundness

GraphRefinement

GraphRunibpEndToEnd

LayerNormDirected

SoundnessProofs

Runtime

Ops

Core

Flatbox

Generative

Diffusion (file)

ForwardGaussian

ImageDDIM

Samplers

Latent (file)

GAN

Objective

VAE

VQVAE

LearningTheory (file)

DifferentialPrivacy (file)

Core

Robustness (file)

Runtime

Spec

Stability (file)

Dynamics (file)

Runtime

Spec

RidgeRegression1D (file)

Real

Core

Optimization

Muon (file)

Certificates

Core

NewtonSchulz

QR

FirstOrder

GDLinearConvergence

OptimizerLaws

SmoothStrongConvexBridge

StronglyConvexGD

Proofs (file)

Approximation (file)

FloatInterval (file)

ConstantTarget

ExactImageTheorem

Semantics

Universal (file)

IEEE32ExecCore

StoneWeierstrass

UniversalApproximation

UniversalApproximationFP32

UniversalApproximationIEEE32Exec

UniversalApproximationIEEE32ExecTwoLayerMlp

UniversalApproximationRate

Hopfield (file)

Basic

Convergence

Dynamics

Energy

Progress

ReLU (file)

Approx

ReLUMulApprox

Approximation

CompactSet

Bridge

ReLUMlpBridge

StateSpace (file)

MambaCausality

Scan

Verification (file)

Robustness (file)

LipschitzCertified

MlpRobustness

SelfSupervised (file)

JEPA

MAE

Masking

PredictiveView

VICReg

API

Proofs (file)

Analysis (file)

Lipschitz (file)

Network

Norm

Dropout

Fft

FftBridge

InductiveProperties

Normalization

Softmax

Autograd

Core

RealCorrectness

SemiringCorrectness

Vectorization

Dual (file)

Domain

FDeriv

Core

Elementwise

Fold

HardMaskedAttention

HardMaskedSoftmax

Interchange

LogSoftmax

MlpMse

OpSpec

Params

PrimitiveArithmetic

PrimitiveCoordinates

PrimitiveExtrema

PrimitiveSpecs

Reindex

Softmax

SoftmaxAxis

SoftmaxSpec

TensorCoordinates

TensorVectorization

Model (file)

Composition

Reverse

Seeding

Runtime

Link (file)

Accumulation

BackwardDense

BackwardDenseGraph

BackwardGraph

BackwardGraphData

BackwardLeaves

BackwardSnoc

Checked

Core

FDeriv

GraphComposition

HigherOrder

HigherOrderFDeriv

HigherOrderReverse

Invariants

ShapeErasure

Tape

Algebra

Nodes

Soundness

Core

FDeriv

Soundness

Nodes (file)

Losses (file)

BCEWithLogits

CrossEntropy

KLDivergence

MSE

NLL

Arithmetic

Batched

Context

Elementwise

GraphComposition

Matrix

Piecewise

Reductions

Shape

Softmax

Ops

Attention

MaskedMultiHeadSelfAttention

MaskedScaledDotProduct

MultiHeadSelfAttention

ScaledDotProduct

SpecBridge

Conv

FDeriv

Index

Embedding

GatherRows

Norm

BatchNorm

BatchNormFDeriv

CtxVecEval

LayerNorm

LayerNormAdjoint

LayerNormBounds

LayerNormEval

LayerNormFDeriv

LayerNormGraph

LayerNormRuntime

MatrixEntries

RowNormalization

Recurrent

ElmanCell

Transformer

DecoderBlock

EncoderBlock

FeedForward

PostNorm

ResidualAttention

Util

Idx

Training

StepAlgebra

Coverage

DualTensor

Notation

Gradients

Activation

Linear

Models (file)

Attention (file)

CausalMask

HardMask

PermutationEquivariance

Weights

Mlp

Probability (file)

DiffusionForward

RL

Algorithms

DQN

Envs

GridWorld

Floats

CheckedRuntime

IEEE32Exec

Boundary

Core

Environment

FiniteStochasticMDP

FinsetSup

Gymnasium

MDP

MarkovMDP

Replay

RuntimeApprox (file)

Core (file)

SpecApprox

Tolerance

FP32 (file)

CROWN

Layers

MLP

Graph (file)

NumericalCertificate (file)

Certificate

Contracts

Enclosure

BackwardApprox

ForwardApprox

LinkAutogradAlgebra

IEEE32

Arithmetic

Contracts

MinMaxTotal

NF (file)

BackwardOps (file)

Backend

Linalg

Main

Sparse

Ops (file)

Elementwise (file)

Binary

Core

SafeDivSigmoid

Softmax

SoftplusSafeLog

Unary

Nodes

Plumbing

Scalar

Sum

Attention

Convolution

EndToEnd

FoldLemmas

Linalg

Normalization

Optimizers

ReductionOps

ShapeOps

SoftmaxAxis

Reductions

IEEE32

Tree

Rounding (file)

RoundingApprox

Scale (file)

BackwardScale

ForwardScale

ScaleApprox

Optimizer

Tensor (file)

Basic (file)

Algebra

BoundsNorms

Core

Factorizations

FactorizationsOrthonormal

FactorizationsReconstruction

Folds

LinearAlgebra

Algebra

AxisAdjoint

AxisLinear

Euclidean

Utils

List

MathFunctions

Verification (file)

ODE (file)

Enclosure

EnclosureBackends

Runtime (file)

Autograd

Engine (file)

Core (file)

ActivationsLoss

Backward

Base

ConvPool

Elementwise

Indexing

Linear

Neural

Shape

Cuda (file)

Ops (file)

Attention

ConvPool

Core

Elementwise

Fourier

Indexing

Linear

NormSoftmax

SelectiveScan

Shape

Buffer

ConvPool

Convert

DGemm

Float32Contract

Fno1dRfftFused

KernelSpec

Kernels

Shape

Tape

Trusted

FastKernels

TapeM

IRExec (file)

Correctness

Ops

Activations

Concat

Constants

Convolution

Elementwise

LinearAlgebra

Loss

Normalization

Permutation

Pooling

Random

Reductions

Structural

Unary

Common

SemanticEquivalence

SemanticEquivalenceCommon

SemanticEquivalenceOpCases

Lowering (file)

Basic

Common

ConvolutionNormalization

Elementwise

LinearAlgebra

Primitives

Reductions

Shape

API

Core

Model (file)

Dual (file)

Nested

Functional (file)

Fourier (file)

Transform

Core

Einsum

EinsumDynamic

SelectiveScan

ShapeOps

Spectral

Layers (file)

Activations

Attention

ConvPool

Core

Mamba

Normalization

Recurrent

Seq

Module (file)

Evaluator

Instantiation

Objective

RuntimeInit

Session (file)

Autograd

Eager

Neural

Ops

ShapeIndex

Types

StateIO (file)

Encoding

Autodiff

Fft

Fno

FnoRfft

Loss

Mamba

Metrics

Norm

Optim

Program

Training

VqVae

Torch (file)

Core (file)

Functional (file)

Activation

Curried

GraphInputs

Layers

Ops

Tensor

Ops (file)

Convolution

Dispatch

Elementwise

Indexing

Layers

LinearAlgebra

Pooling

ShapeReduction

Spectral

OptimizerCheckpoint (file)

CudaAdam

Schema

Session (file)

Backend

Lifecycle

Parameters

Random

Recording

References

State

Trainer (file)

Attention

CheckpointSchema

Eager

EagerOps

Graph

GraphOps

Parameters

Recording

Types

BackwardOptim

CheckpointIO

CudaBridge

ParameterGroups

TensorTransfer

TypedGraph

Types

TypedGraphSession (file)

Autograd

ConvAttention

Core

GraphOps

Neural

ShapeIndex

Initialization

ScalarTrainer

Train (file)

Core

Eval

Logging

Optim

TapeM

Trainer

TypedGraph (file)

GraphM (file)

Convolution

Core

Elementwise

Neural

Pooling

ShapeIndex

Core

LeadingAxis

External (file)

Julia

Optim (file)

Schedulers (file)

Core

Native

PyTorch

Optimizers

PyTorch (file)

Export (file)

CNN

Core

IRPyTorch

MLP

ONNX

StateDict

TorchExport

Transformer

Import (file)

CNN

Core

CrownParamstore

MLP

TorchExport

Transformer

Wire

RL (file)

Algorithms (file)

Bandits

DQN

PolicyGradient

Tabular

ValueLearning

Artifacts

GridWorld (file)

Path

Policy

Position

DefaultPaths

Boundary (file)

Core

Json

DQN

Autograd

Gymnasium (file)

Client

Session

Numerics (file)

Float32 (file)

Advantage

Intervals

PPO

Returns

Types

PPO (file)

Collect

Rollout

Training

PolicyGradient

Autograd

Core

Eval

Replay

Session

Training

Log

Spec (file)

Autograd (file)

AutogradSpec

Ops

Trigonometric

Core (file)

Context (file)

Constants

Rational

Real

FloatInstances (file)

Angle

NF

Tensor (file)

Constructors

Core

Factorizations

Linalg

Numerics

SomeTensor

TensorReductionShape (file)

Broadcasting

ConcatSlice

LinearAlgebra

Reductions

ShapeChange

Complex

Random

Scalar

Sequence

Shape

TensorOps

Dynamics (file)

StateSpace

System

Generative (file)

Diffusion (file)

Core

ForwardProcess

ImageDDIM

Loss

PFODE

ReverseDDIM

ReverseDDPM

Schedule

Latent

Layers (file)

Normalization (file)

BatchNorm

Core

Pooling (file)

Spatial

Activation

Attention

Conv

Dropout

Embedding

FlashAttention

Gnn

Gru

Linear

Loss

Lstm

PositionalEncoding

RealFFT

Rnn

SelectiveScan

Models (file)

Autoencoder

Cnn

Gan

Gmm

Gnn

GradientBoostedTrees

Hmm

Hopfield

Knn

LinearRegression

LogisticRegression

Mamba

Mlp

NaiveBayes

Pca

RandomForest

S4

Seq2seq

Svm

Transformer

Vae

VqVae

Module (file)

Activation

Autoencoder

Conv

Core

DecisionTree

Dropout

Embedding

Flatten

GruModels

Hmm

Linear

LstmModels

Normalization

Pooling

Rnn

RnnModels

Seq2seq

Quantization (file)

Rational

RL (file)

Envs

GridWorld

Core

Environment

FiniteStochasticMDP

MDP

MarkovMDP

Tactic (file)

Autograd (file)

Scalar

Einops (file)

Report (file)

Analysis (file)

Common

Einsum

Pack

ParseShape

Render

Symbolic

Transform

Proof

Verify (file)

Lowering

Converges

Except

Init

Tensor (file)

Internal

Check

Diagnostic

Einsum

Normalize

Pack

ParseShape

Transform

Elab (file)

Einsum (file)

Contraction

Flat

Hoist

Index

Loop

Scalarize

Kernel

Affine

Analysis

Index

Product

Utilities

View

Output (file)

Fusion

Planning

Tiling (file)

Semantics

Width4

Width8

Index

Loop

OutputIndex

Parallel

ParallelOutput

Partition

Planning

Symbolic

Native

Pack (file)

Dispatch

Unpack

Index

Loop

Pointwise

Pull

Reduce

ReductionIndex

Slice

Tensor

Transpose

Transform (file)

Index

View

ViewAttribute

Common

Pack

Syntax

TensorLiteral

Laws (file)

Equivalence (file)

Index

Lowering

Plan

Semantics

MixedRadix

PackIndex

ReductionIndex

RowMajor

Lowering (file)

Einsum (file)

Planning

Reduce (file)

View

Pack

Rearrange

Repeat

TransformFusion

Representation (file)

Basic (file)

Core

Pointwise

Reindex

Traversal

Fiber (file)

Aggregation

Axis

Basic

Differential

Mean

Product

Tie

Coordinate

Promotion

Reduction

Segment

Shape

Storage

Vector

Semantics (file)

Transform (file)

Geometry

RearrangeRepeat

Reduction

Einsum

Pack

Syntax

Parser (file)

Expression (file)

Config

Parse

Roundtrip

Split

State

Einsum

Pack

Transform

Ast

Diagnostic

Lexer

Render

Span

UnicodeData

Interface

Language

Runtime

Constructors

Conversion

Coordinate

LinearAlgebra

Operations

Pack

Packing

Reductions

ShapeErasure

Storage

Testing

Command

Compare

Verification (file)

Builtin

Lowering (file)

API

Builder

Proved (file)

Correctness (file)

Eval (file)

BatchNorm

Concat

Core

Denote

Elementwise

LayerNorm

LinearAlgebra

LoweredNodeBasic

LoweredNodePayload

LoweringPayload

LoweringPrefix

Main

NodeShape

PayloadBridge

PayloadOps

Permutation

Reductions

Return

ShapeOps

Softmax

SourcesAndLosses

Transpose

WellFormed

Lowering

Syntax

Correctness

CrownOpsWorkflow

ExecutableLowering

IBPWorkflow

MlpTrainVerifyWorkflow

TransformerIBPWorkflow

Cert (file)

CROWNQuery (file)

Json

AbCrownLeafCert

CROWNNodeCert

CROWNNodeCertAlphaBeta

IBPCert

IBPNodeCert

NodeReplay

RationalJson

RationalReflection

Geometry3D (file)

Box3D

CLI

LiRPA (file)

Attention

Cnn

ExampleInputs

Gru

Mlp

TransformerEncoder

Monotonicity (file)

Json

ODE (file)

Ast

Parse

Verify

PINN (file)

PyTorch (file)

Load

ParamStore

Architecture

CLI

Certificate

Core

Dataset

DatasetCheck

PdeAst

PdeParse

ResidualAffine

Robustness (file)

Digits

MarginCert

MarginCertCLI

TopLabel

Splines (file)

PiecewiseLinearCLI

PiecewisePolyCert

Util

FloatApprox

Json

Tensor

TextCursor

VNNComp (file)

MnistFC

Spec

CLI

Widgets (file)

Core

Docs

Tensor

UI

IR

ExecutionTrace

Graph

Rewrite

ShapeInference

Interop

PyTorchTranslator

Numerics

Float32

RL

Boundary

GridWorld

PPO

Runtime

Autograd

Training

Verification

CROWN

Docs

Plausible (file)

Arbitrary

ArbitraryFueled

Attr

DeriveArbitrary

DeriveShrinkable

Functions

Gen

Random

Sampleable

Shrinkable

Tactic

Testable

ProofWidgets

Component

Panel

Basic

Basic

FilterDetails

HtmlDisplay

MakeEditLink

OfRpcMethod

RefreshComponent

Data

Html

Cancellable

Compat

Util

Qq (file)

ForLean

Do

ReduceEval

ToExpr

AssertInstancesCommute

Commands

Delab

Macro

Match

MatchImpl

MetaM

Simp

SortLocalDecls

Typ

Std (file)

Async (file)

Basic

ContextAsync

DNS

IO

Process

Select

Signal

System

TCP

Timer

UDP

Data (file)

DHashMap (file)

Internal

AssocList

Basic

Iterator

Lemmas

Defs

HashesTo

Index

Model

Raw

RawLemmas

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawDef

RawLemmas

DTreeMap (file)

Internal

WF

Defs

Lemmas

Balanced

Balancing

Cell

Def

Lemmas

Model

Operations

Ordered

Queries

Zipper

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ExtDHashMap (file)

Basic

Lemmas

ExtDTreeMap (file)

Basic

Lemmas

ExtHashMap (file)

Basic

Lemmas

ExtHashSet (file)

Basic

Lemmas

ExtTreeMap (file)

Basic

Lemmas

ExtTreeSet (file)

Basic

Lemmas

HashMap (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

HashSet (file)

Basic

DecidableEquiv

Iterator

IteratorLemmas

Lemmas

Raw

RawDecidableEquiv

RawLemmas

Internal

List

Associative

Defs

Cut

Iterators (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

StepSize

TakeWhile

Zip

Drop

DropWhile

StepSize

TakeWhile

Zip

Consumers (file)

Monadic (file)

Set

Set

Lemmas (file)

Combinators (file)

Monadic (file)

Drop

DropWhile

FilterMap

TakeWhile

Zip

Drop

DropWhile

TakeWhile

Zip

Consumers (file)

Monadic (file)

Collect

Loop

Set

Collect

Loop

Set

Equivalence (file)

Basic

HetT

StepCongr

Producers (file)

Monadic (file)

Array

Empty

List

Vector

Array

Empty

Range

Repeat

Slice

Vector

Monadic

Producers (file)

Monadic (file)

Array

Empty

Vector

Array

Empty

Range

Repeat

Slice

Vector

String (file)

ToInt

ToNat

TreeMap (file)

Raw (file)

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

TreeSet (file)

Raw (file)

Basic

DecidableEquiv

Iterator

Lemmas

Slice

WF

AdditionalOperations

Basic

DecidableEquiv

Iterator

Lemmas

Slice

ByteSlice

Do (file)

Internal (file)

Ensures (file)

Def

Lemmas

SPred (file)

Notation (file)

Basic

DerivedLaws

Laws

SPred

SVal

Triple (file)

Basic

SpecLemmas

WP (file)

Basic

Monad

SimpLemmas

Sound

PostCond

PredTrans

Http (file)

Data (file)

Body (file)

Any

Basic

Empty

Full

Length

Replayable

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

Redirect

Writer

Server (file)

Config

Connection

Handler

Test

Helpers

Transport

Internal (file)

Do (file)

Gadget

ForIn

Order

Basic

Heyting

Instances

Lemmas

PreservesSup

Triple (file)

Basic

Gadget

SpecLemmas

WP (file)

Basic

Conjunctive

Frame

Lemmas

Assertion

ExceptPost

PredTrans

ForIn (file)

Basic

Lemmas

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

Modifier

Internal (file)

Bounded

UnitVal

Notation (file)

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

Color scheme

darksystemlight