LengthUnit

Statistics

Metric	Count
Definitions `LengthUnit`, `astronomicalUnits`, `centimeters`, `chains`, `feet`, `femtometers`, `furlongs`, `inches`, `instHDivNNReal`, `instInhabited`, `kilometers`, `lightYears`, `links`, `meters`, `micrometers`, `miles`, `millimeters`, `nanometers`, `nauticalMiles`, `parsecs`, `picometers`, `rods`, `scale`, `val`, `yards`	25
Theorems `div_eq_val`, `div_mul_div_coe`, `div_neq_zero`, `div_pos`, `div_self`, `div_symm`, `furlongs_div_yards`, `miles_div_yards`, `property`, `scale_div_scale`, `scale_div_self`, `scale_one`, `scale_scale`, `self_div_scale`, `val_neq_zero`, `val_pos`	16
Total	41

Name	Category	Theorems
`astronomicalUnits` 📖	CompOp	—
`centimeters` 📖	CompOp	—
`chains` 📖	CompOp	—
`feet` 📖	CompOp	—
`femtometers` 📖	CompOp	—
`furlongs` 📖	CompOp	1 math math: `furlongs_div_yards`
`inches` 📖	CompOp	—
`instHDivNNReal` 📖	CompOp	12 math math: `scale_div_scale`, `scale_div_self`, `UnitChoices.dimScale_apply`, `div_symm`, `miles_div_yards`, `div_neq_zero`, `div_eq_val`, `div_pos`, `furlongs_div_yards`, `div_self`, `div_mul_div_coe`, `self_div_scale`
`instInhabited` 📖	CompOp	—
`kilometers` 📖	CompOp	—
`lightYears` 📖	CompOp	—
`links` 📖	CompOp	—
`meters` 📖	CompOp	1 math math: `UnitChoices.SI_length`
`micrometers` 📖	CompOp	—
`miles` 📖	CompOp	1 math math: `miles_div_yards`
`millimeters` 📖	CompOp	—
`nanometers` 📖	CompOp	—
`nauticalMiles` 📖	CompOp	—
`parsecs` 📖	CompOp	—
`picometers` 📖	CompOp	—
`rods` 📖	CompOp	—
`scale` 📖	CompOp	5 math math: `scale_div_scale`, `scale_div_self`, `scale_scale`, `scale_one`, `self_div_scale`
`val` 📖	CompOp	3 math math: `val_pos`, `div_eq_val`, `property`
`yards` 📖	CompOp	2 math math: `miles_div_yards`, `furlongs_div_yards`

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

Name	Category	Theorems
`LengthUnit` 📖	CompData	12 math math: `LengthUnit.scale_div_scale`, `LengthUnit.scale_div_self`, `UnitChoices.dimScale_apply`, `LengthUnit.div_symm`, `LengthUnit.miles_div_yards`, `LengthUnit.div_neq_zero`, `LengthUnit.div_eq_val`, `LengthUnit.div_pos`, `LengthUnit.furlongs_div_yards`, `LengthUnit.div_self`, `LengthUnit.div_mul_div_coe`, `LengthUnit.self_div_scale`

---