Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `WithDim`, `cast`, `instDMulRealHMulDimension`, `instHDivRealHMulDimensionInv`, `instHMulRealHMulDimension`, `instHasDim`, `instMulActionNNReal`, `val`	8
Theorems `cast_refl`, `cast_scaleUnit`, `dim_apply`, `div_scaleUnit`, `ext`, `ext_iff`, `scaleUnit_dim_eq_zero`, `scaleUnit_val`, `scaleUnit_val_eq_scaleUnit_val`, `scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `smul_val`, `val_div_val`, `val_mul_eq_mul`, `val_pow_two_eq_mul`, `withDim_hMul_val`	15
Total	23

WithDim

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	2 math math: `cast_scaleUnit`, `cast_refl`
`instDMulRealHMulDimension` 📖	CompOp	—
`instHDivRealHMulDimensionInv` 📖	CompOp	2 math math: `div_scaleUnit`, `val_div_val`
`instHMulRealHMulDimension` 📖	CompOp	3 math math: `withDim_hMul_val`, `val_mul_eq_mul`, `val_pow_two_eq_mul`
`instHasDim` 📖	CompOp	33 math math: `DimArea.squareFoot_in_SI`, `cast_scaleUnit`, `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `scaleUnit_val`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example2_energyMass`, `DimArea.squareMeter_in_SI`, `scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `scaleUnit_dim_eq_zero`, `UnitExamples.speedEq_isDimensionallyCorrect`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimArea.squareMile_in_SI`, `DimArea.hectare_in_SI`, `scaleUnit_val_eq_scaleUnit_val`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.are_in_SI`, `DimArea.acre_eq_mul_squareFeet`, `DimSpeed.speedOfLight_in_SI`, `dim_apply`, `fderiv_dimension_const_direction`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_in_SI`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `div_scaleUnit`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`
`instMulActionNNReal` 📖	CompOp	33 math math: `DimArea.squareFoot_in_SI`, `cast_scaleUnit`, `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `scaleUnit_val`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example2_energyMass`, `DimArea.squareMeter_in_SI`, `scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `scaleUnit_dim_eq_zero`, `UnitExamples.speedEq_isDimensionallyCorrect`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimArea.squareMile_in_SI`, `DimArea.hectare_in_SI`, `scaleUnit_val_eq_scaleUnit_val`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.are_in_SI`, `DimArea.acre_eq_mul_squareFeet`, `DimSpeed.speedOfLight_in_SI`, `fderiv_dimension_const_direction`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `smul_val`, `DimSpeed.oneKilometerPerHour_in_SI`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `div_scaleUnit`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`
`val` 📖	CompOp	10 math math: `scaleUnit_val`, `scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `scaleUnit_val_eq_scaleUnit_val`, `ext_iff`, `withDim_hMul_val`, `fderiv_dimension_const_direction`, `val_mul_eq_mul`, `val_pow_two_eq_mul`, `smul_val`, `val_div_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_refl` 📖	mathematical	—	`cast` `Dimension`	—	—
`cast_scaleUnit` 📖	mathematical	—	`cast` `UnitDependent.scaleUnit` `WithDim` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instHasDim` `instMulActionNNReal` `instMulUnitDependent`	—	—
`dim_apply` 📖	mathematical	—	`dim` `WithDim` `instHasDim`	—	—
`div_scaleUnit` 📖	mathematical	—	`WithDim` `Dimension` `Dimension.instMul` `Dimension.instCommGroup` `instHDivRealHMulDimensionInv` `UnitDependent.scaleUnit` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instHasDim` `instMulActionNNReal` `instMulUnitDependent`	—	`ext` `val_div_val`
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`scaleUnit_dim_eq_zero` 📖	mathematical	`Dimension` `Dimension.instOne`	`UnitDependent.scaleUnit` `WithDim` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instHasDim` `instMulActionNNReal` `instMulUnitDependent`	—	`ext` `scaleUnit_val` `UnitChoices.dimScale_one`
`scaleUnit_val` 📖	mathematical	—	`val` `UnitDependent.scaleUnit` `WithDim` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instHasDim` `instMulActionNNReal` `instMulUnitDependent` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale`	—	—
`scaleUnit_val_eq_scaleUnit_val` 📖	mathematical	—	`val` `UnitDependent.scaleUnit` `WithDim` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instHasDim` `instMulActionNNReal` `instMulUnitDependent`	—	`ext_iff`
`scaleUnit_val_eq_scaleUnit_val_of_dim_eq` 📖	mathematical	`Dimension`	`val` `UnitDependent.scaleUnit` `WithDim` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instHasDim` `instMulActionNNReal` `instMulUnitDependent`	—	—
`smul_val` 📖	mathematical	—	`val` `WithDim` `instMulActionNNReal`	—	—
`val_div_val` 📖	mathematical	—	`val` `Dimension` `Dimension.instMul` `Dimension.instCommGroup` `WithDim` `instHDivRealHMulDimensionInv`	—	—
`val_mul_eq_mul` 📖	mathematical	—	`val` `Dimension` `Dimension.instMul` `WithDim` `instHMulRealHMulDimension`	—	—
`val_pow_two_eq_mul` 📖	mathematical	—	`val` `Dimension` `Dimension.instMul` `WithDim` `instHMulRealHMulDimension`	—	—
`withDim_hMul_val` 📖	mathematical	—	`val` `Dimension` `Dimension.instMul` `WithDim` `instHMulRealHMulDimension`	—	—

(root)

Definitions

Name	Category	Theorems
`WithDim` 📖	CompData	38 math math: `DimArea.squareFoot_in_SI`, `WithDim.cast_scaleUnit`, `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `WithDim.scaleUnit_val`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example2_energyMass`, `DimArea.squareMeter_in_SI`, `WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `WithDim.scaleUnit_dim_eq_zero`, `UnitExamples.speedEq_isDimensionallyCorrect`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimArea.squareMile_in_SI`, `DimArea.hectare_in_SI`, `WithDim.scaleUnit_val_eq_scaleUnit_val`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.are_in_SI`, `DimArea.acre_eq_mul_squareFeet`, `DimSpeed.speedOfLight_in_SI`, `WithDim.dim_apply`, `WithDim.withDim_hMul_val`, `fderiv_dimension_const_direction`, `WithDim.val_mul_eq_mul`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `WithDim.val_pow_two_eq_mul`, `UnitExamples.cosDim_isDimensionallyCorrect`, `WithDim.smul_val`, `DimSpeed.oneKilometerPerHour_in_SI`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `WithDim.div_scaleUnit`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `WithDim.val_div_val`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`

---

← Back to Index