Documentation Verification Report

Speed

šŸ“ Source: PhysLean/Units/WithDim/Speed.lean

Statistics

MetricCount
DefinitionsDimSpeed, oneKilometerPerHour, oneKnot, oneMeterPerSecond, oneMilePerHour, speedOfLight
6
TheoremsoneKilometerPerHour_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
Total14

DimSpeed

Definitions

NameCategoryTheorems
oneKilometerPerHour šŸ“–CompOp
3 mathmath: oneKilometerPerHour_eq_mul_oneKnot, oneKnot_eq_mul_oneKilometerPerHour, oneKilometerPerHour_in_SI
oneKnot šŸ“–CompOp
3 mathmath: oneKilometerPerHour_eq_mul_oneKnot, oneKnot_eq_mul_oneKilometerPerHour, oneKnot_in_SI
oneMeterPerSecond šŸ“–CompOp
2 mathmath: oneMeterPerSecond_eq_mul_oneMilePerHour, oneMeterPerSecond_in_SI
oneMilePerHour šŸ“–CompOp
2 mathmath: oneMilePerHour_in_SI, oneMeterPerSecond_eq_mul_oneMilePerHour
speedOfLight šŸ“–CompOp
1 mathmath: speedOfLight_in_SI

Theorems

NameKindAssumesProvesValidatesDepends 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

NameCategoryTheorems
DimSpeed šŸ“–CompOp
3 mathmath: DimSpeed.oneKilometerPerHour_eq_mul_oneKnot, DimSpeed.oneKnot_eq_mul_oneKilometerPerHour, DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour

---

← Back to Index