UnitDependent

📁 Source: PhysLean/Units/UnitDependent.lean

Statistics

Metric	Count
Definitions `ContinuousLinearUnitDependent`, `scaleUnitContLinear`, `scaleUnitContLinearEquiv`, `toLinearUnitDependent`, `DMul`, `toHMul`, `DimSet`, `IsDimensionallyCorrect`, `LinearUnitDependent`, `scaleUnitLinear`, `scaleUnitLinearEquiv`, `toUnitDependent`, `MulUnitDependent`, `toUnitDependent`, `UnitDependent`, `scaleUnit`, `scaleUnitEquiv`, `instCarriesDimensionElemDimSet`, `instContinuousLinearUnitDependentContinuousLinearMapRealId`, `instContinuousLinearUnitDependentMap`, `instContinuousLinearUnitDependentOfHasDimOfContinuousConstSMulReal`, `instLinearUnitDependentLinearMapRealId`, `instLinearUnitDependentOfHasDim`, `instMulActionNNRealElemDimSet`, `instMulUnitDependent`, `instUnitDependentForall`, `instUnitDependentForall_1`, `instUnitDependentTwoSided`, `instUnitDependentTwoSidedMul`, `instUnitDependentUnitChoices`	30
Theorems `scaleUnitContLinearEquiv_apply`, `scaleUnitContLinearEquiv_symm_apply`, `scaleUnit_apply_fun`, `scaleUnit_cont`, `hMul_scaleUnit`, `mul_dim`, `mem_iff`, `of_scaleUnit`, `scaleUnit_apply`, `scaleUnit_add`, `scaleUnit_smul`, `scaleUnit_mul`, `dimScale_scaleUnit`, `scaleUnit_apply_fst`, `scaleUnit_apply_fun`, `scaleUnit_apply_fun_left`, `scaleUnit_apply_fun_right`, `scaleUnit_id`, `scaleUnit_injective`, `scaleUnit_symm_apply`, `scaleUnit_trans`, `scaleUnit_trans'`, `isDimensionallyCorrect_fun_iff`, `isDimensionallyCorrect_fun_left`, `isDimensionallyCorrect_fun_right`, `isDimensionallyCorrect_iff`, `scaleUnit_dimSet_val`	27
Total	57

ContinuousLinearUnitDependent

Definitions

Name	Category	Theorems
`scaleUnitContLinear` 📖	CompOp	—
`scaleUnitContLinearEquiv` 📖	CompOp	2 math math: `scaleUnitContLinearEquiv_symm_apply`, `scaleUnitContLinearEquiv_apply`
`toLinearUnitDependent` 📖	CompOp	5 math math: `fderiv_isDimensionallyCorrect`, `scaleUnit_cont`, `scaleUnitContLinearEquiv_symm_apply`, `scaleUnit_apply_fun`, `scaleUnitContLinearEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleUnitContLinearEquiv_apply` 📖	mathematical	—	`scaleUnitContLinearEquiv` `UnitDependent.scaleUnit` `LinearUnitDependent.toUnitDependent` `toLinearUnitDependent`	—	—
`scaleUnitContLinearEquiv_symm_apply` 📖	mathematical	—	`scaleUnitContLinearEquiv` `UnitDependent.scaleUnit` `LinearUnitDependent.toUnitDependent` `toLinearUnitDependent`	—	—
`scaleUnit_apply_fun` 📖	mathematical	—	`UnitDependent.scaleUnit` `LinearUnitDependent.toUnitDependent` `toLinearUnitDependent` `instContinuousLinearUnitDependentMap`	—	—
`scaleUnit_cont` 📖	mathematical	—	`UnitDependent.scaleUnit` `LinearUnitDependent.toUnitDependent` `toLinearUnitDependent`	—	—

DMul

Definitions

Name	Category	Theorems
`toHMul` 📖	CompOp	2 math math: `mul_dim`, `hMul_scaleUnit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hMul_scaleUnit` 📖	mathematical	—	`toHMul` `UnitDependent.scaleUnit` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instMulUnitDependent`	—	`mul_dim` `CarriesDimension.toDimensionful_apply_apply` `UnitChoices.dimScale_self` `UnitChoices.dimScale_mul_symm`
`mul_dim` 📖	mathematical	—	`HasDimension` `toHMul`	—	—

DimSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_iff` 📖	mathematical	—	`DimSet` `UnitDependent.scaleUnit` `MulUnitDependent.toUnitDependent` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale`	—	—

Dimensionful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_scaleUnit` 📖	mathematical	—	`HasDimension` `UnitDependent.scaleUnit` `UnitChoices` `instUnitDependentUnitChoices` `CarriesDimension.toMulAction` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale` `dim` `CarriesDimension.toHasDim`	—	`UnitChoices.dimScale_scaleUnit`

HasDim

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleUnit_apply` 📖	mathematical	—	`UnitDependent.scaleUnit` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instMulUnitDependent` `Dimension` `Dimension.instCommGroup` `UnitChoices.dimScale` `dim` `CarriesDimension.toHasDim`	—	`CarriesDimension.toDimensionful_apply_apply`

LinearUnitDependent

Definitions

Name	Category	Theorems
`scaleUnitLinear` 📖	CompOp	—
`scaleUnitLinearEquiv` 📖	CompOp	—
`toUnitDependent` 📖	CompOp	8 math math: `scaleUnit_add`, `ContinuousLinearUnitDependent.scaleUnit_cont`, `ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_symm_apply`, `integral_isDimensionallyCorrect`, `ContinuousLinearUnitDependent.scaleUnit_apply_fun`, `scaleUnit_smul`, `ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_apply`, `scaleUnit_measure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleUnit_add` 📖	mathematical	—	`UnitDependent.scaleUnit` `toUnitDependent`	—	—
`scaleUnit_smul` 📖	mathematical	—	`UnitDependent.scaleUnit` `toUnitDependent`	—	—

MulUnitDependent

Definitions

Name	Category	Theorems
`toUnitDependent` 📖	CompOp	24 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`, `DMul.hMul_scaleUnit`, `WithDim.scaleUnit_val_eq_scaleUnit_val`, `scaleUnit_mul`, `fderiv_dimension_const_direction`, `HasDim.scaleUnit_apply`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `scaleUnit_measure`, `UnitExamples.cosDim_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `WithDim.div_scaleUnit`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `DimSet.mem_iff`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleUnit_mul` 📖	mathematical	—	`UnitDependent.scaleUnit` `toUnitDependent`	—	—

UnitChoices

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimScale_scaleUnit` 📖	mathematical	—	`Dimension` `Dimension.instCommGroup` `dimScale` `UnitDependent.scaleUnit` `UnitChoices` `instUnitDependentUnitChoices`	—	`LengthUnit.self_div_scale` `LengthUnit.val_pos` `TimeUnit.self_div_scale` `TimeUnit.val_pos` `MassUnit.self_div_scale` `MassUnit.val_pos` `ChargeUnit.self_div_scale` `ChargeUnit.val_pos` `TemperatureUnit.self_div_scale` `TemperatureUnit.val_pos`
`scaleUnit_apply_fst` 📖	mathematical	—	`UnitDependent.scaleUnit` `UnitChoices` `instUnitDependentUnitChoices`	—	`ext`

UnitDependent

Definitions

Name	Category	Theorems
`scaleUnit` 📖	CompOp	35 math math: `WithDim.cast_scaleUnit`, `scaleUnit_apply_fun`, `WithDim.scaleUnit_val`, `LinearUnitDependent.scaleUnit_add`, `ContinuousLinearUnitDependent.scaleUnit_cont`, `ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_symm_apply`, `scaleUnit_trans'`, `isDimensionallyCorrect_fun_iff`, `scaleUnit_dimSet_val`, `ContinuousLinearUnitDependent.scaleUnit_apply_fun`, `UnitExamples.example2_energyMass`, `WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_eq`, `WithDim.scaleUnit_dim_eq_zero`, `LinearUnitDependent.scaleUnit_smul`, `scaleUnit_trans`, `ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_apply`, `scaleUnit_apply_fun_left`, `DMul.hMul_scaleUnit`, `Dimensionful.of_scaleUnit`, `UnitChoices.scaleUnit_apply_fst`, `WithDim.scaleUnit_val_eq_scaleUnit_val`, `UnitChoices.dimScale_scaleUnit`, `MulUnitDependent.scaleUnit_mul`, `scaleUnit_apply_fun_right`, `scaleUnit_injective`, `isDimensionallyCorrect_fun_right`, `HasDim.scaleUnit_apply`, `fderiv_apply_scaleUnit`, `scaleUnit_measure`, `scaleUnit_id`, `isDimensionallyCorrect_iff`, `WithDim.div_scaleUnit`, `DimSet.mem_iff`, `isDimensionallyCorrect_fun_left`, `scaleUnit_symm_apply`
`scaleUnitEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleUnit_apply_fun` 📖	mathematical	—	`scaleUnit` `instUnitDependentTwoSided`	—	—
`scaleUnit_apply_fun_left` 📖	mathematical	—	`scaleUnit` `instUnitDependentForall_1`	—	—
`scaleUnit_apply_fun_right` 📖	mathematical	—	`scaleUnit` `instUnitDependentForall`	—	—
`scaleUnit_id` 📖	mathematical	—	`scaleUnit`	—	—
`scaleUnit_injective` 📖	mathematical	—	`scaleUnit`	—	`scaleUnit_symm_apply`
`scaleUnit_symm_apply` 📖	mathematical	—	`scaleUnit`	—	`scaleUnit_trans` `scaleUnit_id`
`scaleUnit_trans` 📖	mathematical	—	`scaleUnit`	—	—
`scaleUnit_trans'` 📖	mathematical	—	`scaleUnit`	—	—

(root)

Definitions

Name	Category	Theorems
`ContinuousLinearUnitDependent` 📖	CompData	—
`DMul` 📖	CompData	—
`DimSet` 📖	CompOp	3 math math: `integral_isDimensionallyCorrect`, `scaleUnit_dimSet_val`, `DimSet.mem_iff`
`IsDimensionallyCorrect` 📖	MathDef	14 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `isDimensionallyCorrect_fun_iff`, `integral_isDimensionallyCorrect`, `UnitExamples.speedEq_isDimensionallyCorrect`, `isDimensionallyCorrect_fun_right`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `isDimensionallyCorrect_iff`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `isDimensionallyCorrect_fun_left`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`
`LinearUnitDependent` 📖	CompData	—
`MulUnitDependent` 📖	CompData	—
`UnitDependent` 📖	CompData	—
`instCarriesDimensionElemDimSet` 📖	CompOp	2 math math: `integral_isDimensionallyCorrect`, `scaleUnit_dimSet_val`
`instContinuousLinearUnitDependentContinuousLinearMapRealId` 📖	CompOp	—
`instContinuousLinearUnitDependentMap` 📖	CompOp	2 math math: `fderiv_isDimensionallyCorrect`, `ContinuousLinearUnitDependent.scaleUnit_apply_fun`
`instContinuousLinearUnitDependentOfHasDimOfContinuousConstSMulReal` 📖	CompOp	1 math math: `fderiv_isDimensionallyCorrect`
`instLinearUnitDependentLinearMapRealId` 📖	CompOp	—
`instLinearUnitDependentOfHasDim` 📖	CompOp	2 math math: `integral_isDimensionallyCorrect`, `scaleUnit_measure`
`instMulActionNNRealElemDimSet` 📖	CompOp	—
`instMulUnitDependent` 📖	CompOp	21 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`, `DMul.hMul_scaleUnit`, `WithDim.scaleUnit_val_eq_scaleUnit_val`, `fderiv_dimension_const_direction`, `HasDim.scaleUnit_apply`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `WithDim.div_scaleUnit`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`
`instUnitDependentForall` 📖	CompOp	2 math math: `UnitDependent.scaleUnit_apply_fun_right`, `isDimensionallyCorrect_fun_right`
`instUnitDependentForall_1` 📖	CompOp	12 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `UnitExamples.speedEq_isDimensionallyCorrect`, `UnitDependent.scaleUnit_apply_fun_left`, `fderiv_dimension_const_direction`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `isDimensionallyCorrect_fun_left`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`
`instUnitDependentTwoSided` 📖	CompOp	12 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `UnitDependent.scaleUnit_apply_fun`, `UnitExamples.energyMassWithDimNot_not_isDimensionallyCorrect`, `UnitExamples.oddDimensions_isDimensionallyCorrect`, `isDimensionallyCorrect_fun_iff`, `integral_isDimensionallyCorrect`, `UnitExamples.speedEq_isDimensionallyCorrect`, `UnitExamples.energyMassWithDim'_isDimensionallyCorrect`, `UnitExamples.cosDim_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim'_isDimensionallyCorrect`, `UnitExamples.newtonsSecondWithDim_isDimensionallyCorrect`, `UnitExamples.energyMassWithDim_isDimensionallyCorrect`
`instUnitDependentTwoSidedMul` 📖	CompOp	1 math math: `integral_isDimensionallyCorrect`
`instUnitDependentUnitChoices` 📖	CompOp	4 math math: `UnitExamples.energyMass_isDimensionallyCorrect`, `Dimensionful.of_scaleUnit`, `UnitChoices.scaleUnit_apply_fst`, `UnitChoices.dimScale_scaleUnit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDimensionallyCorrect_fun_iff` 📖	mathematical	—	`IsDimensionallyCorrect` `instUnitDependentTwoSided` `UnitDependent.scaleUnit`	—	—
`isDimensionallyCorrect_fun_left` 📖	mathematical	—	`IsDimensionallyCorrect` `instUnitDependentForall_1` `UnitDependent.scaleUnit`	—	—
`isDimensionallyCorrect_fun_right` 📖	mathematical	—	`IsDimensionallyCorrect` `instUnitDependentForall` `UnitDependent.scaleUnit`	—	—
`isDimensionallyCorrect_iff` 📖	mathematical	—	`IsDimensionallyCorrect` `UnitDependent.scaleUnit`	—	—
`scaleUnit_dimSet_val` 📖	mathematical	—	`DimSet` `UnitDependent.scaleUnit` `MulUnitDependent.toUnitDependent` `CarriesDimension.toMulAction` `instCarriesDimensionElemDimSet` `instMulUnitDependent`	—	`HasDim.scaleUnit_apply`

---

← Back to Index