Documentation Verification Report

Basic

📁 Source: Mathlib/Data/FP/Basic.lean

Statistics

Metric	Count
Definitions `Float`, `add`, `div`, `instAdd`, `instNeg`, `instSub`, `isFinite`, `isZero`, `mul`, `neg`, `sign`, `sign'`, `sub`, `zero`, `FloatCfg`, `emax`, `prec`, `RMode`, `ValidFinite`, `decValidFinite`, `divNatLtTwoPow`, `emax`, `emin`, `instInhabitedFloat`, `instInhabitedRMode`, `default`, `nextDn`, `nextDnPos`, `nextUp`, `nextUpPos`, `ofPosRatDn`, `ofRat`, `ofRatDn`, `ofRatUp`, `prec`, `toRat`, `shift2`	37
Theorems `valid`, `precMax`, `precPos`	3
Total	40

FP

Definitions

Name	Category	Theorems
`Float` 📖	CompData	—
`FloatCfg` 📖	CompData	—
`RMode` 📖	CompData	—
`ValidFinite` 📖	MathDef	1 math math: `Float.Zero.valid`
`decValidFinite` 📖	CompOp	—
`divNatLtTwoPow` 📖	CompOp	—
`emax` 📖	CompOp	—
`emin` 📖	CompOp	1 math math: `Float.Zero.valid`
`instInhabitedFloat` 📖	CompOp	—
`instInhabitedRMode` 📖	CompOp	—
`nextDn` 📖	CompOp	—
`nextDnPos` 📖	CompOp	—
`nextUp` 📖	CompOp	—
`nextUpPos` 📖	CompOp	—
`ofPosRatDn` 📖	CompOp	—
`ofRat` 📖	CompOp	—
`ofRatDn` 📖	CompOp	—
`ofRatUp` 📖	CompOp	—
`prec` 📖	CompOp	—
`toRat` 📖	CompOp	—

FP.Float

Definitions

Name	Category	Theorems
`add` 📖	CompOp	—
`div` 📖	CompOp	—
`instAdd` 📖	CompOp	—
`instNeg` 📖	CompOp	—
`instSub` 📖	CompOp	—
`isFinite` 📖	CompOp	—
`isZero` 📖	CompOp	—
`mul` 📖	CompOp	—
`neg` 📖	CompOp	—
`sign` 📖	CompOp	—
`sign'` 📖	CompOp	—
`sub` 📖	CompOp	—
`zero` 📖	CompOp	—

FP.Float.Zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`valid` 📖	mathematical	—	`FP.ValidFinite` `FP.emin`	—	`add_sub_assoc` `le_add_of_nonneg_right` `Int.instAddLeftMono` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `Int.ofNat_le_ofNat_of_le` `FP.FloatCfg.precPos` `le_trans` `FP.FloatCfg.precMax` `sub_nonneg` `Nat.size_zero` `Nat.cast_zero` `add_zero` `sub_eq_add_neg` `sup_of_le_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`

FP.FloatCfg

Definitions

Name	Category	Theorems
`emax` 📖	CompOp	1 math math: `precMax`
`prec` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`precMax` 📖	mathematical	—	`emax`	—	—
`precPos` 📖	—	—	—	—	—

FP.instInhabitedRMode

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Int

Definitions

Name	Category	Theorems
`shift2` 📖	CompOp	—

---

← Back to Index