General documentation

index
foundational types
tactics

Library

TauCeti
Algebra
AlgebraicGroup
AdditiveFrobeniusKernel
Basic
ReducedPoints
AdditiveGroup
BaseChange
Basic
BaseChange
Basic
Naturality
CommHopfAlgCat
BaseChange
Basic
DiagonalizableGroup
BaseChange
Basic
Functoriality
FiniteType
BaseChange
CommHopfAlgCat
Product
GroupAlgebra
NotReduced
Product
Hopf
KernelPoints
Map
HopfIdeal
Points
Basic
Naturality
Order
Quotient
Basic
Order
MultiplicativeGroup
BaseChange
Basic
RootsOfUnity
BaseChange
Basic
Inclusion
Kernel
SplitTorus
BaseChange
Basic
Cocharacter
Cocharacter
FunctorOfPoints
PointsFunctor
Product
Trivial
Bialgebra
MonoidAlgebraProduct
Quotient
TensorProduct
Category
CommAlgCat
RestrictScalars
Coalgebra
Comodule
Finite
Basic
Cofree
Corestrict
Preadditive
Product
MatrixCoefficient
Adjoin
Basic
Functorial
Product
Regular
TensorProduct
Transport
Trivial
Basic
Cat
Cofree
Corestrict
Hom
Preadditive
Product
Regular
TensorProduct
Transport
Trivial
Zero
Subcoalgebra
Basic
GroupLike
Lattice
Map
RegularSubcomodule
Subcomodule
Basic
Comap
Induced
Lattice
Quotient
Group
ElementaryTwoQuotient
Basic
Cyclic
FreeModule
Prod
NormalizerQuotient
Basic
Conjugation
FreeAbelianCharacter
PowMonoidHom
ZMultiples
GroupAction
FiniteSupportPerm
FixingSubgroup
OrbitRelQuotient
HopfAlgebra
HopfIdeal
Basic
Comap
Basic
Kernel
SymmetricAlgebra
Polynomial
Card
BoundedCoeff
RootSetUnion
Squarefree
AlgebraicGeometry
AbelianVariety
Hom (file)
BaseChange
Basic
Basic
MorphismGroup
WeilDivisor
AbelJacobi
Sum
BasepointChange
Basic
Basic
DegreeSplitting
FiniteSum
FixedDegree
LinearSystem
Quotient
Dedekind
Basic
ClassGroup
Degree
Image
Basic
Splitting
Order
Splitting
ZeroGenerators
FixedDegree
Addition
Basic
Subtraction
LinearSystem
Addition
Basic
Monotone
Principal
Basic
Kernel
BasepointChange
Basic
Common
FiniteSum
FractionalIdealDivisor
Order
PicZeroQuotient
PositiveNegativeFixedDegree
Union
IrreducibleOfConnectedDomainStalk
AlgebraicTopology
FundamentalGroup
BasepointChange
Basic
Homeomorph
Product
SemilocallySimplyConnected
Basic
On
SimplicialComplex
Collapse (file)
Basic
FaceCount
Simplex
Basic
Link
Basic
Dimension
ElementaryCollapse
Join
LinkStar
Maps
UniversalCover
Circle
FundamentalGroup
NotSimplyConnected
Deck
Connected
Basic
Torsor
Fiber
Basic
Orbit
TorsorTransport
Transport
FundamentalGroup
Basic
Opposite
NormalSubgroupFiberQuotient
Basic
Equivariance
NormalizerQuotient
Conjugation
FiberAction
Quotient
Basic
Covering
Homeomorph
Regular
Basic
Torsor
SubgroupFiberOrbit
Basic
QuotientGroup
Basic
Conjugation
AddCircle
BasedPath
Basic
ComplexCircleFundamentalGroup
PathHomotopyDiscreteness
TorusFundamentalGroup
NotSimplyConnected
Analysis
Bochner
CharFun
PosDef
PositiveDefinite
FourierConvention
Gaussian
Calculus
DSlopeIntegral
DerivativeTest
HalfLinePrimitive
IteratedDerivWithin
OneSidedDerivLimit
CompletelyMonotone
Bernstein
Basic
Integral
Measures
Basic
Closure
Integral
OpenClosure
Power
Reciprocal
Reparametrization
Complex
Conformal
Hyperbolic
Distance
Triangle
Reflection (file)
Circle (file)
Basic
Conjugate
Basic
Principle
SchwarzPick
AutomorphismIsometry
Basic
Derivative
Isometry
UnitDisc
Automorphism
Basic
Classification
Rotation
Homeomorph
Moebius
PoincareMetricSpace
PseudoHyperbolic
UnitDisc
Basic
Contour
Argument
Lift
Principle
Cauchy
PrincipalValue
Basic
On
Goursat
IntegralFormula
Chord
QuotientAsymptotics
TangentBound
Crossing
Finiteness
Monotonicity
PVAggregation
Windows
Curve
Distance
IntegralBound
Reparam
Dixon
H2
Bound
Diff
Def
FunctionDiff
H1Diff
Liouville
HigherOrder
Asymptotics
CPV
PerWindow
CPV
HigherOrder
PolarPart
CPV
Decomposition
Residue
Assembly
Basic
LogDeriv
SimplePole
Theorem
Winding
Number
Affine
Basic
Circle
Concat
Reparam
Reverse
Scale
Translate
Continuity
CrossingValue
Integer
Integrand
LocallyConstant
RealIntegral
SegmentSum
Vanishing
WorkedExamples
TwoSimplePoles
ArcFTC
ConditionDischarge
ExitTime
FlatnessOne
HomologyCauchy
HungerbuhlerWasem
InvSubCPVExistence
LogDerivFTC
MeromorphicLaurent
ModelSectorWinding
NullHomologous
PiecewiseC1On
PwC1ImmersionOn
RegularityConditions
SectorCancellation
TangentForcing
WindowSplitting
Fredholm
Basic
Prod
Splitting
InnerProductSpace
Harmonic
Ball
Dilation
Isometry
Laplacian
Basic
Comparison
DriftMaximumPrinciple
LocalExtr
LowerOrderMaximumPrinciple
MaximumPrinciple
WeakMaximumPrinciple
ZerothOrderMaximumPrinciple
HilbertBasisMap
L2Product
LaxMilgram
WeightedOrthogonalBasis
Normed
Module
Ball
PDE
EnergyForm
Basic
Continuity
Integrability
Linearity
Lp
Measurability
VariableLp
Integrated
EnergyForm
SymmetricEnergy
Uniform
EllipticEnergy
Ellipticity
EnergyLowerBounds
LowerOrder
ShiftedLaplacianEnergy
SymmetricEnergy
PositiveDefinite
Function
Closure
Kernel
Kernel
Basic
Bounds
Closure
Finsupp
Radical
SemigroupGroup
Time
Axis
Slice
Basic
Bounds
FourierLaplace
Normalize
Product
Pullback
Basic
Continuity
FourierAtom
Limits
Normalize
Pullback
Semigroups
BoundedGenerator (file)
Basic
Resolvent
Generator (file)
Basic
Invariance
OrbitDerivative
Resolvent
Basic
Identity
PowerBounds
Basic
CauchyProblem
Defs
ExponentialShift
GrowthBound
Identity
SpecialFunctions
Hermite
Function
Basic
Ladder
Lp
MemLp
Orthonormal
Oscillator
Orthogonality
Trigonometric
Chebyshev
CosineTransfer
Measure
Moments
Span
Data
Finset
Basic
Setoid
Basic
Sym
Basic
FieldTheory
IntermediateField
AdjoinEqTop
Card
Quadratic
SquareClassGroup
Trace
Geometry
Diffeomorphism
Action
Congr
FixingSubgroup
Group
RelativeCongr
Manifold
SmoothEmbedding
AmbientIsotopy
Defs
Prod
ContinuousAmbientIsotopy
Basic
Naturality
Prod
Basic
Symplectic
Complex
Module
Basic
Hom
Line
JHolomorphic
Prod
Basic
Map
Basic
Congruence
Conj
Energy
Line
MapOps
Neg
Square
Transport
Lagrangian
Basic
Constructions
Graph
Prod
TotallyReal
Transport
Prod
Basic
Metric
AlmostComplex
CompatibleMetric
Finrank
Hermitian
Rescale
StandardCompatible
SymplecticTransport
TameMetric
TotallyReal
Transport
KnotTheory
Grid
Commutation
Basic
Move
Relabeling
Rotation
Diagram
Basic
Relabeling
Differential
Square
Backtracking
Coefficient
Support
Support
Basic
Cardinality
Symmetry
Grading
Change
Integer
JFunction
Basic
Count
Rectangle
Basic
Count
Swap
SmallGrid
Differential
Gradings
BasicCycles
BlockedRectangle
ChainCardinality
Complex
CycleSymmetry
Cycles
CyclicInterval
Gradings
Homology
Rotation
StateCardinality
LinearAlgebra
Complex
Finrank
LinearPart
TotallyReal
LowDimTopology
Plumbing
Cube
Face
Basic
Exponent
Weight
Basic
Recursion
Cardinality
Generator
VertexWeight
Weight
Basic
Polarization
Translation
Characteristic
Conjugation
IntersectionForm
NegativeDefinite
MeasureTheory
Function
AEStronglyMeasurable
BoundedMemLp
BoundedSupportExponential
ConditionalExpectation
LpBilinearForm
PolynomialMemLp
WeightL2Isometry
Measure
ProductKernel
Prokhorov
NumberTheory
ClassGroup
ElementaryTwoQuotient
Equiv
DedekindDomain
RamificationInertia
Transversal
EffectiveBounds
ClassNumber
Basic
UnitSquares
Discriminant
Basic
Corollaries
Equality
HermiteCount
Basic
Monotone
NatAbs
Threshold
IdealCount
Basic
Corollaries
Quadratic
ClassNumber
Basic
UnitSquares
Discriminant
UnitSquares
Basic
Corollaries
Regulator
SimpleGenerators
TraceForm
WorkedExamples
GeometryOfNumbers
Doubling
RankTwoDoubling
LegendreSymbol
Frobenius
SquareClass
Multiquadratic
CMField
Basic
GaloisGroup
FundamentalDiscriminant
Basic
Examples
Factorization
OfSquarefree
Galois
Basic
Exponent
Group
Legendre
PrimeDiscriminant
Basic
Examples
EvenPrimeDiscriminant
PrimeDiscriminants
MinusTwentyOne
Examples
Galois
Prime
Discriminant
Examples
Basic
Lists
Roots
Basic
DegreeExamples
GaloisGroup
Independence
Splitting
SubfieldLattice
Subfield
Count
Degree
Lattice
Discriminants
GaloisGroup
RadicandSplitting
Radicands
SquareClass
Basic
Independence
Subfield
Classification
Count
Degree
Lattice
CoprimeSquarefree
Degree
EvenPrimeDiscriminant
Frobenius
GenusField
MultiquadraticSplitting
QuadraticSubfield
RelativeDegree
NumberField
Internal
PrimeDivisibility
QuadraticIntegralBasis
Units
Dirichlet
ElementaryTwoQuotient
ClassGroupElementaryTwoQuotient
Frobenius
IntegralSqrt
QuadraticSplitting
SplitsCompletely
RamificationInertia
Galois
Probability
DeFinetti
DirectingMeasure
Basic
Coord
BlockFactorization
CommonEnding
CondExpConvergence
FutureFactorization
PrefixDeletion
TailFactorization
Theorem
Distributions
Gaussian
HermiteMemLp
PolynomialMemLp
Ergodic
FixedSpace
KoopmanMarkov
Exchangeability
ConditionallyIID
Basic
Implications
Map
L2
BlockAverages
BoundedObservable
Covariance
LongTailAverages
PathSpace
Exchangeable
Sigma
ToContractable
Law
Basic
Bridge
ContractableLaw
ProcessShift
Shift
AdjacentTranspositions
Basic
Contractability
Cylinder
ExchangeableAtMonotone
FiniteMarginals
FullyExchangeable
IID
Map
PermutationExtension
Stationary
ThreeCycle
Independence
Conditional
Martingale
Crossings
Bounds
Pathwise
TimeReversal
AntitoneLimit
Convergence
LevyDownwardEventuallyConst
Reverse
Moments
Determinacy
Process
Tail
Basic
ReverseFiltration
RingTheory
Ideal
LiesOver
Polynomial
Chebyshev
Basis
Hermite
Derivative
GeneratingFunction
Topology
Algebra
Homeomorph
Action
Congr
ConstMulAction
Homotopy
AmbientIsotopic
Basic
Naturality
HomotopyGroup
Homeomorph
Homotopy
Map
Isotopy
Basic
Comp
Prod
AmbientIsotopyConj
Covering
Cube
Path

Color scheme