Basic

Statistics

Metric	Count
Definitions `CarriesDimension`, `toDimensionful`, `toHasDim`, `toMulAction`, `Dimensionful`, `HasDim`, `d`, `HasDimension`, `UnitChoices`, `SI`, `SIPrimed`, `charge`, `dimScale`, `length`, `mass`, `temperature`, `time`, `dim`, `instCoeFunDimensionfulForallUnitChoices`, `instMulActionNNRealDimensionful`	20
Theorems `toDimensionful_apply_apply`, `ext`, `ext_iff`, `smul_apply`, `SI_charge`, `SI_length`, `SI_mass`, `SI_temperature`, `SI_time`, `dimScale_SIPrimed_SI`, `dimScale_SI_SIPrimed`, `dimScale_apply`, `dimScale_coe_mul_symm`, `dimScale_mul_symm`, `dimScale_neq_zero`, `dimScale_of_inv_eq_swap`, `dimScale_one`, `dimScale_pos`, `dimScale_self`, `dimScale_symm`, `dimScale_transitive`, `ext`, `ext_iff`, `smul_dimScale_injective`, `hasDimension_iff`	25
Total	45

CarriesDimension

Definitions

Name	Category	Theorems
`toDimensionful` 📖	CompOp	1 math math: `toDimensionful_apply_apply`
`toHasDim` 📖	CompOp	4 math math: `toDimensionful_apply_apply`, `Dimensionful.of_scaleUnit`, `HasDim.scaleUnit_apply`, `hasDimension_iff`
`toMulAction` 📖	CompOp	25 math math: `WithDim.cast_scaleUnit`, `UnitExamples.energyMass_isDimensionallyCorrect`, `WithDim.scaleUnit_val`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `integral_isDimensionallyCorrect`, `scaleUnit_dimSet_val`, `UnitExamples.example2_energyMass`, `WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `WithDim.scaleUnit_dim_eq_zero`, `UnitExamples.speedEq_isDimensionallyCorrect`, `toDimensionful_apply_apply`, `DMul.hMul_scaleUnit`, `Dimensionful.of_scaleUnit`, `WithDim.scaleUnit_val_eq_scaleUnit_val`, `fderiv_dimension_const_direction`, `HasDim.scaleUnit_apply`, `hasDimension_iff`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `Dimensionful.smul_apply`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `WithDim.div_scaleUnit`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toDimensionful_apply_apply` 📖	mathematical	—	`HasDimension` `Dimensionful` `toDimensionful` `toMulAction` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale` `dim` `toHasDim`	—	—

Dimensionful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`HasDimension`	—	—	—
`ext_iff` 📖	mathematical	—	`HasDimension`	—	`ext`
`smul_apply` 📖	mathematical	—	`HasDimension` `Dimensionful` `instMulActionNNRealDimensionful` `CarriesDimension.toMulAction`	—	—

HasDim

Definitions

Name	Category	Theorems
`d` 📖	CompOp	—

UnitChoices

Definitions

Name	Category	Theorems
`SI` 📖	CompOp	20 math math: `DimArea.squareFoot_in_SI`, `dimScale_SI_SIPrimed`, `DimSpeed.oneMilePerHour_in_SI`, `UnitExamples.example1_energyMass`, `UnitExamples.example2_energyMass`, `DimArea.squareMeter_in_SI`, `SI_temperature`, `SI_charge`, `DimArea.squareMile_in_SI`, `DimArea.hectare_in_SI`, `dimScale_SIPrimed_SI`, `DimArea.are_in_SI`, `SI_length`, `DimSpeed.speedOfLight_in_SI`, `SI_mass`, `SI_time`, `DimSpeed.oneKilometerPerHour_in_SI`, `DimSpeed.oneMeterPerSecond_in_SI`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`
`SIPrimed` 📖	CompOp	2 math math: `dimScale_SI_SIPrimed`, `dimScale_SIPrimed_SI`
`charge` 📖	CompOp	3 math math: `ext_iff`, `dimScale_apply`, `SI_charge`
`dimScale` 📖	CompOp	20 math math: `dimScale_SI_SIPrimed`, `WithDim.scaleUnit_val`, `dimScale_of_inv_eq_swap`, `dimScale_coe_mul_symm`, `dimScale_self`, `dimScale_apply`, `dimScale_one`, `CarriesDimension.toDimensionful_apply_apply`, `Dimensionful.of_scaleUnit`, `dimScale_scaleUnit`, `dimScale_pos`, `dimScale_SIPrimed_SI`, `dimScale_transitive`, `HasDim.scaleUnit_apply`, `fderiv_apply_scaleUnit`, `hasDimension_iff`, `dimScale_mul_symm`, `dimScale_symm`, `DimSet.mem_iff`, `smul_dimScale_injective`
`length` 📖	CompOp	3 math math: `ext_iff`, `dimScale_apply`, `SI_length`
`mass` 📖	CompOp	3 math math: `ext_iff`, `dimScale_apply`, `SI_mass`
`temperature` 📖	CompOp	3 math math: `ext_iff`, `dimScale_apply`, `SI_temperature`
`time` 📖	CompOp	3 math math: `ext_iff`, `dimScale_apply`, `SI_time`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SI_charge` 📖	mathematical	—	`charge` `SI` `ChargeUnit.coulombs`	—	—
`SI_length` 📖	mathematical	—	`length` `SI` `LengthUnit.meters`	—	—
`SI_mass` 📖	mathematical	—	`mass` `SI` `MassUnit.kilograms`	—	—
`SI_temperature` 📖	mathematical	—	`temperature` `SI` `TemperatureUnit.kelvin`	—	—
`SI_time` 📖	mathematical	—	`time` `SI` `TimeUnit.seconds`	—	—
`dimScale_SIPrimed_SI` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale` `SIPrimed` `SI` `Dimension.length` `Dimension.time` `Dimension.mass` `Dimension.charge` `Dimension.temperature`	—	`LengthUnit.scale_div_self` `TimeUnit.scale_div_self` `MassUnit.scale_div_self` `ChargeUnit.scale_div_self` `TemperatureUnit.scale_div_self`
`dimScale_SI_SIPrimed` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale` `SI` `SIPrimed` `Dimension.length` `Dimension.time` `Dimension.mass` `Dimension.charge` `Dimension.temperature`	—	`LengthUnit.self_div_scale` `TimeUnit.self_div_scale` `MassUnit.self_div_scale` `ChargeUnit.self_div_scale` `TemperatureUnit.self_div_scale`
`dimScale_apply` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale` `LengthUnit` `LengthUnit.instHDivNNReal` `length` `Dimension.length` `TimeUnit` `TimeUnit.instHDivNNReal` `time` `Dimension.time` `MassUnit` `MassUnit.instHDivNNReal` `mass` `Dimension.mass` `ChargeUnit` `ChargeUnit.instHDivNNReal` `charge` `Dimension.charge` `TemperatureUnit` `TemperatureUnit.instHDivNNReal` `temperature` `Dimension.temperature`	—	—
`dimScale_coe_mul_symm` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	`dimScale_mul_symm`
`dimScale_mul_symm` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	`dimScale_transitive` `dimScale_self`
`dimScale_neq_zero` 📖	—	—	—	—	—
`dimScale_of_inv_eq_swap` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	`dimScale_symm`
`dimScale_one` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale` `Dimension.instOne`	—	—
`dimScale_pos` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	`dimScale_neq_zero`
`dimScale_self` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	`LengthUnit.div_self` `TimeUnit.div_self` `MassUnit.div_self` `ChargeUnit.div_self` `TemperatureUnit.div_self`
`dimScale_symm` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	`LengthUnit.div_symm` `TimeUnit.div_symm` `MassUnit.div_symm` `ChargeUnit.div_symm` `TemperatureUnit.div_symm`
`dimScale_transitive` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	—
`ext` 📖	—	`length` `time` `mass` `charge` `temperature`	—	—	—
`ext_iff` 📖	mathematical	—	`length` `time` `mass` `charge` `temperature`	—	`ext`
`smul_dimScale_injective` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale`	—	—

(root)

Definitions

Name	Category	Theorems
`CarriesDimension` 📖	CompData	—
`Dimensionful` 📖	CompOp	2 math math: `CarriesDimension.toDimensionful_apply_apply`, `Dimensionful.smul_apply`
`HasDim` 📖	CompData	—
`HasDimension` 📖	MathDef	17 math math: `DimArea.squareFoot_in_SI`, `DMul.mul_dim`, `DimSpeed.oneMilePerHour_in_SI`, `DimArea.squareMeter_in_SI`, `CarriesDimension.toDimensionful_apply_apply`, `DimArea.squareMile_in_SI`, `Dimensionful.of_scaleUnit`, `DimArea.hectare_in_SI`, `DimArea.are_in_SI`, `DimSpeed.speedOfLight_in_SI`, `hasDimension_iff`, `Dimensionful.ext_iff`, `DimSpeed.oneKilometerPerHour_in_SI`, `Dimensionful.smul_apply`, `DimSpeed.oneMeterPerSecond_in_SI`, `DimSpeed.oneKnot_in_SI`, `DimArea.acre_in_SI`
`UnitChoices` 📖	CompData	4 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `Dimensionful.of_scaleUnit`, `UnitChoices.scaleUnit_apply_fst`, `UnitChoices.dimScale_scaleUnit`
`dim` 📖	CompOp	8 math math: `integral_isDimensionallyCorrect`, `CarriesDimension.toDimensionful_apply_apply`, `Dimensionful.of_scaleUnit`, `WithDim.dim_apply`, `fderiv_dimension_const_direction`, `HasDim.scaleUnit_apply`, `fderiv_apply_scaleUnit`, `hasDimension_iff`
`instCoeFunDimensionfulForallUnitChoices` 📖	CompOp	—
`instMulActionNNRealDimensionful` 📖	CompOp	5 math math: `DimSpeed.oneKilometerPerHour_eq_mul_oneKnot`, `DimSpeed.oneKnot_eq_mul_oneKilometerPerHour`, `DimSpeed.oneMeterPerSecond_eq_mul_oneMilePerHour`, `DimArea.acre_eq_mul_squareFeet`, `Dimensionful.smul_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasDimension_iff` 📖	mathematical	—	`HasDimension` `CarriesDimension.toMulAction` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale` `dim` `CarriesDimension.toHasDim`	—	—

---

← Back to Index