Dimension

📁 Source: PhysLean/Units/Dimension.lean

Statistics

Metric	Count
Definitions `Dimension`, `C𝓭`, `L𝓭`, `M𝓭`, `T𝓭`, `charge`, `instCommGroup`, `instMul`, `instOne`, `instPowRat`, `length`, `mass`, `temperature`, `time`, `Θ𝓭`	15
Theorems `L𝓭_charge`, `L𝓭_length`, `L𝓭_mass`, `L𝓭_temperature`, `L𝓭_time`, `T𝓭_charge`, `T𝓭_length`, `T𝓭_mass`, `T𝓭_temperature`, `T𝓭_time`, `charge_mul`, `div_charge`, `div_length`, `div_mass`, `div_temperature`, `div_time`, `ext`, `ext_iff`, `inv_charge`, `inv_length`, `inv_mass`, `inv_temperature`, `inv_time`, `length_mul`, `mass_mul`, `npow_charge`, `npow_length`, `npow_mass`, `npow_temperature`, `npow_time`, `one_charge`, `one_length`, `one_mass`, `one_temperature`, `one_time`, `temperature_mul`, `time_mul`	37
Total	52

Dimension

Definitions

Name	Category	Theorems
`C𝓭` 📖	CompOp	1 math math: `UnitExamples.oddDimensions_isDimensionallyCorrect`
`L𝓭` 📖	CompOp	30 math math: `DimArea.squareFoot_in_SI`, `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `L𝓭_charge`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example1_energyMass`, `L𝓭_time`, `UnitExamples.example2_energyMass`, `DimArea.squareMeter_in_SI`, `UnitExamples.speedEq_isDimensionallyCorrect`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimArea.squareMile_in_SI`, `DimArea.hectare_in_SI`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.are_in_SI`, `L𝓭_temperature`, `DimArea.acre_eq_mul_squareFeet`, `L𝓭_length`, `DimSpeed.speedOfLight_in_SI`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `L𝓭_mass`, `DimSpeed.oneKilometerPerHour_in_SI`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`
`M𝓭` 📖	CompOp	9 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `UnitExamples.example1_energyMass`, `UnitExamples.example2_energyMass`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`
`T𝓭` 📖	CompOp	24 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example1_energyMass`, `T𝓭_mass`, `UnitExamples.example2_energyMass`, `T𝓭_length`, `UnitExamples.speedEq_isDimensionallyCorrect`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `T𝓭_time`, `T𝓭_temperature`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimSpeed.speedOfLight_in_SI`, `T𝓭_charge`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_in_SI`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `DimSpeed.oneKnot_in_SI`
`charge` 📖	CompOp	11 math math: `UnitChoices.dimScale_SI_SIPrimed`, `L𝓭_charge`, `one_charge`, `charge_mul`, `ext_iff`, `UnitChoices.dimScale_apply`, `npow_charge`, `UnitChoices.dimScale_SIPrimed_SI`, `T𝓭_charge`, `div_charge`, `inv_charge`
`instCommGroup` 📖	CompOp	58 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `UnitChoices.dimScale_SI_SIPrimed`, `WithDim.scaleUnit_val`, `UnitChoices.dimScale_of_inv_eq_swap`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `UnitChoices.dimScale_coe_mul_symm`, `UnitChoices.dimScale_self`, `DimSpeed.oneMilePerHour_in_SI`, `inv_mass`, `UnitExamples.example1_energyMass`, `integral_isDimensionallyCorrect`, `UnitExamples.example2_energyMass`, `inv_length`, `UnitExamples.speedEq_isDimensionallyCorrect`, `UnitChoices.dimScale_apply`, `UnitChoices.dimScale_one`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `npow_charge`, `CarriesDimension.toDimensionful_apply_apply`, `Dimensionful.of_scaleUnit`, `UnitChoices.dimScale_scaleUnit`, `UnitChoices.dimScale_pos`, `npow_mass`, `UnitChoices.dimScale_SIPrimed_SI`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimSpeed.speedOfLight_in_SI`, `div_temperature`, `UnitChoices.dimScale_transitive`, `fderiv_dimension_const_direction`, `div_charge`, `HasDim.scaleUnit_apply`, `fderiv_apply_scaleUnit`, `hasDimension_iff`, `inv_time`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `div_mass`, `npow_time`, `npow_temperature`, `npow_length`, `UnitExamples.cosDim_isDimensionallyCorrect`, `inv_charge`, `DimSpeed.oneKilometerPerHour_in_SI`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `WithDim.div_scaleUnit`, `UnitChoices.dimScale_mul_symm`, `UnitChoices.dimScale_symm`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `WithDim.val_div_val`, `div_length`, `DimSet.mem_iff`, `UnitChoices.smul_dimScale_injective`, `inv_temperature`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `div_time`, `DimSpeed.oneKnot_in_SI`
`instMul` 📖	CompOp	37 math math: `DimArea.squareFoot_in_SI`, `temperature_mul`, `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example1_energyMass`, `charge_mul`, `integral_isDimensionallyCorrect`, `UnitExamples.example2_energyMass`, `DimArea.squareMeter_in_SI`, `UnitExamples.speedEq_isDimensionallyCorrect`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimArea.squareMile_in_SI`, `DimArea.hectare_in_SI`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.are_in_SI`, `DimArea.acre_eq_mul_squareFeet`, `DimSpeed.speedOfLight_in_SI`, `length_mul`, `WithDim.withDim_hMul_val`, `fderiv_dimension_const_direction`, `mass_mul`, `WithDim.val_mul_eq_mul`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `WithDim.val_pow_two_eq_mul`, `time_mul`, `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`
`instOne` 📖	CompOp	6 math math: `one_temperature`, `one_charge`, `one_length`, `one_mass`, `UnitChoices.dimScale_one`, `one_time`
`instPowRat` 📖	CompOp	—
`length` 📖	CompOp	11 math math: `UnitChoices.dimScale_SI_SIPrimed`, `inv_length`, `ext_iff`, `one_length`, `T𝓭_length`, `UnitChoices.dimScale_apply`, `UnitChoices.dimScale_SIPrimed_SI`, `L𝓭_length`, `length_mul`, `npow_length`, `div_length`
`mass` 📖	CompOp	11 math math: `UnitChoices.dimScale_SI_SIPrimed`, `inv_mass`, `T𝓭_mass`, `ext_iff`, `one_mass`, `UnitChoices.dimScale_apply`, `npow_mass`, `UnitChoices.dimScale_SIPrimed_SI`, `mass_mul`, `div_mass`, `L𝓭_mass`
`temperature` 📖	CompOp	11 math math: `temperature_mul`, `UnitChoices.dimScale_SI_SIPrimed`, `one_temperature`, `ext_iff`, `UnitChoices.dimScale_apply`, `T𝓭_temperature`, `UnitChoices.dimScale_SIPrimed_SI`, `L𝓭_temperature`, `div_temperature`, `npow_temperature`, `inv_temperature`
`time` 📖	CompOp	11 math math: `UnitChoices.dimScale_SI_SIPrimed`, `L𝓭_time`, `ext_iff`, `UnitChoices.dimScale_apply`, `T𝓭_time`, `UnitChoices.dimScale_SIPrimed_SI`, `inv_time`, `npow_time`, `time_mul`, `one_time`, `div_time`
`Θ𝓭` 📖	CompOp	1 math math: `UnitExamples.oddDimensions_isDimensionallyCorrect`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`L𝓭_charge` 📖	mathematical	—	`charge` `L𝓭`	—	—
`L𝓭_length` 📖	mathematical	—	`length` `L𝓭`	—	—
`L𝓭_mass` 📖	mathematical	—	`mass` `L𝓭`	—	—
`L𝓭_temperature` 📖	mathematical	—	`temperature` `L𝓭`	—	—
`L𝓭_time` 📖	mathematical	—	`time` `L𝓭`	—	—
`T𝓭_charge` 📖	mathematical	—	`charge` `T𝓭`	—	—
`T𝓭_length` 📖	mathematical	—	`length` `T𝓭`	—	—
`T𝓭_mass` 📖	mathematical	—	`mass` `T𝓭`	—	—
`T𝓭_temperature` 📖	mathematical	—	`temperature` `T𝓭`	—	—
`T𝓭_time` 📖	mathematical	—	`time` `T𝓭`	—	—
`charge_mul` 📖	mathematical	—	`charge` `Dimension` `instMul`	—	—
`div_charge` 📖	mathematical	—	`charge` `Dimension` `instCommGroup`	—	`charge_mul` `inv_charge`
`div_length` 📖	mathematical	—	`length` `Dimension` `instCommGroup`	—	`length_mul` `inv_length`
`div_mass` 📖	mathematical	—	`mass` `Dimension` `instCommGroup`	—	`mass_mul` `inv_mass`
`div_temperature` 📖	mathematical	—	`temperature` `Dimension` `instCommGroup`	—	`temperature_mul` `inv_temperature`
`div_time` 📖	mathematical	—	`time` `Dimension` `instCommGroup`	—	`time_mul` `inv_time`
`ext` 📖	—	`length` `time` `mass` `charge` `temperature`	—	—	—
`ext_iff` 📖	mathematical	—	`length` `time` `mass` `charge` `temperature`	—	`ext`
`inv_charge` 📖	mathematical	—	`charge` `Dimension` `instCommGroup`	—	—
`inv_length` 📖	mathematical	—	`length` `Dimension` `instCommGroup`	—	—
`inv_mass` 📖	mathematical	—	`mass` `Dimension` `instCommGroup`	—	—
`inv_temperature` 📖	mathematical	—	`temperature` `Dimension` `instCommGroup`	—	—
`inv_time` 📖	mathematical	—	`time` `Dimension` `instCommGroup`	—	—
`length_mul` 📖	mathematical	—	`length` `Dimension` `instMul`	—	—
`mass_mul` 📖	mathematical	—	`mass` `Dimension` `instMul`	—	—
`npow_charge` 📖	mathematical	—	`charge` `Dimension` `instCommGroup`	—	—
`npow_length` 📖	mathematical	—	`length` `Dimension` `instCommGroup`	—	—
`npow_mass` 📖	mathematical	—	`mass` `Dimension` `instCommGroup`	—	—
`npow_temperature` 📖	mathematical	—	`temperature` `Dimension` `instCommGroup`	—	—
`npow_time` 📖	mathematical	—	`time` `Dimension` `instCommGroup`	—	—
`one_charge` 📖	mathematical	—	`charge` `Dimension` `instOne`	—	—
`one_length` 📖	mathematical	—	`length` `Dimension` `instOne`	—	—
`one_mass` 📖	mathematical	—	`mass` `Dimension` `instOne`	—	—
`one_temperature` 📖	mathematical	—	`temperature` `Dimension` `instOne`	—	—
`one_time` 📖	mathematical	—	`time` `Dimension` `instOne`	—	—
`temperature_mul` 📖	mathematical	—	`temperature` `Dimension` `instMul`	—	—
`time_mul` 📖	mathematical	—	`time` `Dimension` `instMul`	—	—

(root)

Definitions

Name	Category	Theorems
`Dimension` 📖	CompData	79 math math: `DimArea.squareFoot_in_SI`, `Dimension.temperature_mul`, `UnitExamples.energyMass_isDimensionallyCorrect`, `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `UnitChoices.dimScale_SI_SIPrimed`, `WithDim.scaleUnit_val`, `UnitChoices.dimScale_of_inv_eq_swap`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `UnitChoices.dimScale_coe_mul_symm`, `UnitChoices.dimScale_self`, `DimSpeed.oneMilePerHour_in_SI`, `Dimension.one_temperature`, `Dimension.inv_mass`, `UnitExamples.example1_energyMass`, `Dimension.one_charge`, `Dimension.charge_mul`, `integral_isDimensionallyCorrect`, `UnitExamples.example2_energyMass`, `Dimension.inv_length`, `DimArea.squareMeter_in_SI`, `Dimension.one_length`, `UnitExamples.speedEq_isDimensionallyCorrect`, `Dimension.one_mass`, `UnitChoices.dimScale_apply`, `UnitChoices.dimScale_one`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `Dimension.npow_charge`, `CarriesDimension.toDimensionful_apply_apply`, `DimArea.squareMile_in_SI`, `Dimensionful.of_scaleUnit`, `DimArea.hectare_in_SI`, `WithDim.cast_refl`, `UnitChoices.dimScale_scaleUnit`, `UnitChoices.dimScale_pos`, `Dimension.npow_mass`, `UnitChoices.dimScale_SIPrimed_SI`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.are_in_SI`, `DimArea.acre_eq_mul_squareFeet`, `DimSpeed.speedOfLight_in_SI`, `Dimension.div_temperature`, `Dimension.length_mul`, `WithDim.withDim_hMul_val`, `UnitChoices.dimScale_transitive`, `fderiv_dimension_const_direction`, `Dimension.mass_mul`, `WithDim.val_mul_eq_mul`, `Dimension.div_charge`, `HasDim.scaleUnit_apply`, `fderiv_apply_scaleUnit`, `hasDimension_iff`, `Dimension.inv_time`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `Dimension.div_mass`, `Dimension.npow_time`, `Dimension.npow_temperature`, `WithDim.val_pow_two_eq_mul`, `Dimension.npow_length`, `UnitExamples.cosDim_isDimensionallyCorrect`, `Dimension.time_mul`, `Dimension.inv_charge`, `DimSpeed.oneKilometerPerHour_in_SI`, `Dimension.one_time`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `WithDim.div_scaleUnit`, `UnitChoices.dimScale_mul_symm`, `UnitChoices.dimScale_symm`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSpeed.oneMeterPerSecond_in_SI`, `WithDim.val_div_val`, `Dimension.div_length`, `DimSet.mem_iff`, `UnitChoices.smul_dimScale_injective`, `Dimension.inv_temperature`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`, `Dimension.div_time`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`

---

← Back to Index