Documentation Verification Report

Speed

📁 Source: PhysLean/Units/WithDim/Speed.lean

Statistics

Metric	Count
Definitions `DimSpeed`, `oneKilometerPerHour`, `oneKnot`, `oneMeterPerSecond`, `oneMilePerHour`, `speedOfLight`	6
Theorems `oneKilometerPerHour_eq_mul_oneKnot`, `oneKilometerPerHour_in_SI`, `oneKnot_eq_mul_oneKilometerPerHour`, `oneKnot_in_SI`, `oneMeterPerSecond_eq_mul_oneMilePerHour`, `oneMeterPerSecond_in_SI`, `oneMilePerHour_in_SI`, `speedOfLight_in_SI`	8
Total	14

DimSpeed

Definitions

Name	Category	Theorems
`oneKilometerPerHour` 📖	CompOp	3 math math: `oneKilometerPerHour_eq_mul_oneKnot`, `oneKnot_eq_mul_oneKilometerPerHour`, `oneKilometerPerHour_in_SI`
`oneKnot` 📖	CompOp	3 math math: `oneKilometerPerHour_eq_mul_oneKnot`, `oneKnot_eq_mul_oneKilometerPerHour`, `oneKnot_in_SI`
`oneMeterPerSecond` 📖	CompOp	2 math math: `oneMeterPerSecond_eq_mul_oneMilePerHour`, `oneMeterPerSecond_in_SI`
`oneMilePerHour` 📖	CompOp	2 math math: `oneMilePerHour_in_SI`, `oneMeterPerSecond_eq_mul_oneMilePerHour`
`speedOfLight` 📖	CompOp	1 math math: `speedOfLight_in_SI`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`oneKilometerPerHour_eq_mul_oneKnot` 📖	mathematical	—	`oneKilometerPerHour` `DimSpeed` `instMulActionNNRealDimensionful` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneKnot`	—	`oneKilometerPerHour_in_SI` `oneKnot_in_SI` `WithDim.ext`
`oneKilometerPerHour_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneKilometerPerHour` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `LengthUnit.scale_div_self` `TimeUnit.scale_div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self` `Dimension.L𝓭_length` `Dimension.T𝓭_length` `Dimension.L𝓭_time` `Dimension.T𝓭_time` `WithDim.ext`
`oneKnot_eq_mul_oneKilometerPerHour` 📖	mathematical	—	`oneKnot` `DimSpeed` `instMulActionNNRealDimensionful` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneKilometerPerHour`	—	`oneKnot_in_SI` `oneKilometerPerHour_in_SI` `WithDim.ext`
`oneKnot_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneKnot` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `LengthUnit.scale_div_self` `TimeUnit.scale_div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self` `Dimension.L𝓭_length` `Dimension.T𝓭_length` `Dimension.L𝓭_time` `Dimension.T𝓭_time` `WithDim.ext`
`oneMeterPerSecond_eq_mul_oneMilePerHour` 📖	mathematical	—	`oneMeterPerSecond` `DimSpeed` `instMulActionNNRealDimensionful` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneMilePerHour`	—	`oneMeterPerSecond_in_SI` `oneMilePerHour_in_SI` `WithDim.ext`
`oneMeterPerSecond_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneMeterPerSecond` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `UnitChoices.dimScale_self`
`oneMilePerHour_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `oneMilePerHour` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `LengthUnit.scale_div_self` `TimeUnit.scale_div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self` `Dimension.L𝓭_length` `Dimension.T𝓭_length` `Dimension.L𝓭_time` `Dimension.T𝓭_time` `WithDim.ext`
`speedOfLight_in_SI` 📖	mathematical	—	`HasDimension` `WithDim` `Dimension` `Dimension.instMul` `Dimension.L𝓭` `Dimension.instCommGroup` `Dimension.T𝓭` `WithDim.instHasDim` `WithDim.instMulActionNNReal` `speedOfLight` `UnitChoices.SI`	—	`CarriesDimension.toDimensionful_apply_apply` `UnitChoices.dimScale_self`

(root)

Definitions

Name	Category	Theorems
`DimSpeed` 📖	CompOp	3 math math: `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`

---

← Back to Index