Documentation Verification Report

MassUnit

📁 Source: PhysLean/ClassicalMechanics/Mass/MassUnit.lean

Statistics

Metric	Count
Definitions `MassUnit`, `grams`, `hundredweights`, `instHDivNNReal`, `instInhabited`, `kilograms`, `longTons`, `metricTons`, `micrograms`, `milligrams`, `nominalSolarMasses`, `ounces`, `pounds`, `quarters`, `scale`, `shortTons`, `stones`, `val`	18
Theorems `div_eq_val`, `div_mul_div_coe`, `div_neq_zero`, `div_pos`, `div_self`, `div_symm`, `longTons_div_kilograms`, `pounds_div_ounces`, `property`, `scale_div_scale`, `scale_div_self`, `scale_one`, `scale_scale`, `self_div_scale`, `shortTons_div_kilograms`, `val_neq_zero`, `val_pos`	17
Total	35

MassUnit

Definitions

Name	Category	Theorems
`grams` 📖	CompOp	—
`hundredweights` 📖	CompOp	—
`instHDivNNReal` 📖	CompOp	13 math math: `scale_div_self`, `self_div_scale`, `div_mul_div_coe`, `longTons_div_kilograms`, `UnitChoices.dimScale_apply`, `shortTons_div_kilograms`, `div_eq_val`, `pounds_div_ounces`, `scale_div_scale`, `div_symm`, `div_pos`, `div_self`, `div_neq_zero`
`instInhabited` 📖	CompOp	—
`kilograms` 📖	CompOp	3 math math: `longTons_div_kilograms`, `shortTons_div_kilograms`, `UnitChoices.SI_mass`
`longTons` 📖	CompOp	1 math math: `longTons_div_kilograms`
`metricTons` 📖	CompOp	—
`micrograms` 📖	CompOp	—
`milligrams` 📖	CompOp	—
`nominalSolarMasses` 📖	CompOp	—
`ounces` 📖	CompOp	1 math math: `pounds_div_ounces`
`pounds` 📖	CompOp	1 math math: `pounds_div_ounces`
`quarters` 📖	CompOp	—
`scale` 📖	CompOp	5 math math: `scale_div_self`, `self_div_scale`, `scale_one`, `scale_div_scale`, `scale_scale`
`shortTons` 📖	CompOp	1 math math: `shortTons_div_kilograms`
`stones` 📖	CompOp	—
`val` 📖	CompOp	3 math math: `property`, `val_pos`, `div_eq_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_eq_val` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `val` `val_pos`	—	—
`div_mul_div_coe` 📖	mathematical	—	`MassUnit` `instHDivNNReal`	—	—
`div_neq_zero` 📖	mathematical	—	`MassUnit` `instHDivNNReal`	—	`val_pos` `div_eq_val`
`div_pos` 📖	mathematical	—	`MassUnit` `instHDivNNReal`	—	`div_neq_zero`
`div_self` 📖	mathematical	—	`MassUnit` `instHDivNNReal`	—	`val_pos` `val_neq_zero`
`div_symm` 📖	mathematical	—	`MassUnit` `instHDivNNReal`	—	`val_pos` `div_eq_val`
`longTons_div_kilograms` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `longTons` `kilograms`	—	`scale_scale` `scale_div_self`
`pounds_div_ounces` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `pounds` `ounces`	—	`scale_div_scale` `div_self`
`property` 📖	mathematical	—	`val`	—	—
`scale_div_scale` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `scale`	—	—
`scale_div_self` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `scale`	—	`val_pos`
`scale_one` 📖	mathematical	—	`scale`	—	—
`scale_scale` 📖	mathematical	—	`scale`	—	—
`self_div_scale` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `scale`	—	`val_pos`
`shortTons_div_kilograms` 📖	mathematical	—	`MassUnit` `instHDivNNReal` `shortTons` `kilograms`	—	`scale_scale` `scale_div_self`
`val_neq_zero` 📖	—	—	—	—	`property`
`val_pos` 📖	mathematical	—	`val`	—	`property`

(root)

Definitions

Name	Category	Theorems
`MassUnit` 📖	CompData	13 math math: `MassUnit.scale_div_self`, `MassUnit.self_div_scale`, `MassUnit.div_mul_div_coe`, `MassUnit.longTons_div_kilograms`, `UnitChoices.dimScale_apply`, `MassUnit.shortTons_div_kilograms`, `MassUnit.div_eq_val`, `MassUnit.pounds_div_ounces`, `MassUnit.scale_div_scale`, `MassUnit.div_symm`, `MassUnit.div_pos`, `MassUnit.div_self`, `MassUnit.div_neq_zero`

---

← Back to Index