Interactive definition DAG. Definition dependencies and theorem uses are separate from proof premises.
- ND0291 — BetaZeroExtend
- ND0292 — PolynomialDiagonalTerm
- ND0293 — PolynomialDiagonalPrefix
- ND0382 — IRatValid
- ND0383 — IRatEq
- ND0388 — IQuadProductReal
- ND0389 — IQuadProductRadical
- ND0390 — IQuadAt
- ND0391 — IQuadProductStep
- ND0392 — IQuadProductTrace
- ND0393 — IQuadNonzeroFactors
- ND0394 — IQuadCanonicalProduct
- ND0395 — IQuadHeight
- ND0396 — IQuadCanonicalStep
- ND0397 — IQuadCanonicalTrace
- ND0398 — IQuadHeightBound
- ND0399 — IQuadFactorHeightBound
- ND0400 — NatExpAtanhRecurrence
- ND0401 — NatConvolutionCoefficient
- ND0402 — NatConvolutionPrefix
- ND0403 — NatUnitCoefficient
- ND0404 — NatUnitPrefix
- ND0405 — NatPowerRow
- ND0406 — NatPowerStep
- ND0407 — NatPowerTrace
- ND0408 — NatZeroBefore
- ND0409 — NatLinearTriple
- ND0410 — NatEulerPrefix
- ND0411 — NatAffineSlice
- ND0412 — NatAffineSum
- ND0413 — NatAffineRowSums
- ND0414 — NatTripleCell
- ND0415 — NatTripleFlatCell
- ND0416 — NatTripleFlatPrefix
- ND0417 — NatTripleGrid
- ND0418 — NatTripleRowPrefix
- ND0419 — NatZeroPrefix
- ND0420 — NatWeightedSeriesStep
- ND0421 — NatWeightedSeriesTrace
- ND0422 — NatShiftedEulerPrefix
- ND0423 — NatExpWeightTable
- ND0424 — NatAtanhCoefficient
- ND0425 — NatAtanhPrefix
- ND0426 — NatScaledHornerStep
- ND0427 — NatScaledHornerTrace
- ND0428 — NatGeometricWeightTable
- ND0429 — NatHornerWeightedPrefix
- ND0430 — NatCauchyCell
- ND0431 — NatCauchyFlatCell
- ND0432 — NatCauchyFlatPrefix
- ND0433 — NatCauchyGrid
- ND0434 — NatCauchyRow
- ND0435 — NatCauchyColumn
- ND0436 — NatZeroAfter
- ND0437 — NatHornerValue
- ND0438 — NatRowHornerPrefix
- ND0439 — NatPointwiseProductPrefix
- ND0440 — NatBoundedPrefix
- ND0441 — NatRatioBoundPrefix
- ND0442 — NatPowerWeightedPrefix
- ND0443 — NatScaledExpRecurrence
- ND0444 — IRatLe
- ND0445 — NatLinearBound
- ND0446 — DyadicSqrt2
- ND0447 — NatSqrt2LogArgument
- ND0448 — NatSqrt2ExpSample
- ND0449 — NatSqrt2ApproxRecord
- PD0001 — Le
- PD0002 — Lt
- PD0013 — BetaAt
- PD0014 — Product
- PD0015 — Sum
- PD0018 — Range
- PD0019 — Repeat
- PD0020 — Pow
- PD0023 — Factorial
- PD0051 — FloorSqrt