Documentation Verification Report

TemperatureUnits

📁 Source: PhysLean/Thermodynamics/Temperature/TemperatureUnits.lean

Statistics

Metric	Count
Definitions `TemperatureUnit`, `absoluteFahrenheit`, `instHDivNNReal`, `instInhabited`, `kelvin`, `microkelvin`, `millikelvin`, `nanokelvin`, `scale`, `val`	10
Theorems `div_eq_val`, `div_mul_div_coe`, `div_neq_zero`, `div_pos`, `div_self`, `div_symm`, `property`, `scale_div_scale`, `scale_div_self`, `scale_one`, `scale_scale`, `self_div_scale`, `val_neq_zero`, `val_pos`	14
Total	24

TemperatureUnit

Definitions

Name	Category	Theorems
`absoluteFahrenheit` 📖	CompOp	—
`instHDivNNReal` 📖	CompOp	10 math math: `self_div_scale`, `scale_div_scale`, `div_neq_zero`, `div_mul_div_coe`, `div_pos`, `UnitChoices.dimScale_apply`, `div_self`, `div_eq_val`, `scale_div_self`, `div_symm`
`instInhabited` 📖	CompOp	—
`kelvin` 📖	CompOp	1 math math: `UnitChoices.SI_temperature`
`microkelvin` 📖	CompOp	—
`millikelvin` 📖	CompOp	—
`nanokelvin` 📖	CompOp	—
`scale` 📖	CompOp	5 math math: `scale_one`, `self_div_scale`, `scale_div_scale`, `scale_scale`, `scale_div_self`
`val` 📖	CompOp	3 math math: `val_pos`, `div_eq_val`, `property`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_eq_val` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal` `val` `val_pos`	—	—
`div_mul_div_coe` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal`	—	—
`div_neq_zero` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal`	—	`val_pos` `div_eq_val`
`div_pos` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal`	—	`div_neq_zero`
`div_self` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal`	—	`val_pos` `val_neq_zero`
`div_symm` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal`	—	`val_pos` `div_eq_val`
`property` 📖	mathematical	—	`val`	—	—
`scale_div_scale` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal` `scale`	—	—
`scale_div_self` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal` `scale`	—	`val_pos`
`scale_one` 📖	mathematical	—	`scale`	—	—
`scale_scale` 📖	mathematical	—	`scale`	—	—
`self_div_scale` 📖	mathematical	—	`TemperatureUnit` `instHDivNNReal` `scale`	—	`val_pos`
`val_neq_zero` 📖	—	—	—	—	`property`
`val_pos` 📖	mathematical	—	`val`	—	`property`

(root)

Definitions

Name	Category	Theorems
`TemperatureUnit` 📖	CompData	10 math math: `TemperatureUnit.self_div_scale`, `TemperatureUnit.scale_div_scale`, `TemperatureUnit.div_neq_zero`, `TemperatureUnit.div_mul_div_coe`, `TemperatureUnit.div_pos`, `UnitChoices.dimScale_apply`, `TemperatureUnit.div_self`, `TemperatureUnit.div_eq_val`, `TemperatureUnit.scale_div_self`, `TemperatureUnit.div_symm`

---

← Back to Index