Examples

📁 Source: PhysLean/Units/Examples.lean

Statistics

Metric	Count
Definitions CosDim, EnergyMass, EnergyMass', EnergyMassWithDim, EnergyMassWithDim', EnergyMassWithDimNot, NewtonsSecondWithDim, NewtonsSecondWithDim', OddDimensions, SpeedEq, meters400	11
Theorems cosDim_isDimensionallyCorrect, energyMassWithDim'_isDimensionallyCorrect, energyMassWithDimNot_not_isDimensionallyCorrect, energyMassWithDim_isDimensionallyCorrect, energyMass_isDimensionallyCorrect, example1_energyMass, example2_energyMass, newtonsSecondWithDim'_isDimensionallyCorrect, newtonsSecondWithDim_isDimensionallyCorrect, oddDimensions_isDimensionallyCorrect, speedEq_isDimensionallyCorrect	11
Total	22

UnitExamples

Definitions

Name	Category	Theorems
CosDim 📖	MathDef	1 math math: cosDim_isDimensionallyCorrect
EnergyMass 📖	MathDef	3 math math: energyMass_isDimensionallyCorrect, example1_energyMass, example2_energyMass
EnergyMass' 📖	MathDef	—
EnergyMassWithDim 📖	MathDef	1 math math: energyMassWithDim_isDimensionallyCorrect
EnergyMassWithDim' 📖	MathDef	1 math math: energyMassWithDim'_isDimensionallyCorrect
EnergyMassWithDimNot 📖	MathDef	1 math math: energyMassWithDimNot_not_isDimensionallyCorrect
NewtonsSecondWithDim 📖	MathDef	1 math math: newtonsSecondWithDim_isDimensionallyCorrect
NewtonsSecondWithDim' 📖	MathDef	1 math math: newtonsSecondWithDim'_isDimensionallyCorrect
OddDimensions 📖	MathDef	1 math math: oddDimensions_isDimensionallyCorrect
SpeedEq 📖	MathDef	1 math math: speedEq_isDimensionallyCorrect
meters400 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cosDim_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.T𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent instUnitDependentForall_1 Dimension Dimension.instCommGroup CosDim	—	WithDim.val_mul_eq_mul DMul.hMul_scaleUnit WithDim.scaleUnit_dim_eq_zero
energyMassWithDim'_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 instUnitDependentForall_1 EnergyMassWithDim'	—	WithDim.cast.congr_simp DMul.hMul_scaleUnit WithDim.cast_scaleUnit
energyMassWithDimNot_not_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 instUnitDependentForall_1 EnergyMassWithDimNot	—	UnitChoices.dimScale_SIPrimed_SI Dimension.L𝓭_length Dimension.T𝓭_length Dimension.L𝓭_time Dimension.T𝓭_time Dimension.L𝓭_mass Dimension.T𝓭_mass Dimension.L𝓭_charge Dimension.T𝓭_charge Dimension.L𝓭_temperature Dimension.T𝓭_temperature
energyMassWithDim_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 instUnitDependentForall_1 EnergyMassWithDim	—	WithDim.val_pow_two_eq_mul DMul.hMul_scaleUnit WithDim.val_mul_eq_mul WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_eq Dimension.ext Dimension.L𝓭_length Dimension.T𝓭_length Dimension.L𝓭_time Dimension.T𝓭_time Dimension.L𝓭_mass Dimension.T𝓭_mass Dimension.L𝓭_charge Dimension.T𝓭_charge Dimension.L𝓭_temperature Dimension.T𝓭_temperature
energyMass_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 instUnitDependentForall_1 UnitChoices instUnitDependentUnitChoices EnergyMass	—	HasDim.scaleUnit_apply Dimensionful.of_scaleUnit WithDim.val_pow_two_eq_mul WithDim.val_mul_eq_mul Dimension.ext Dimension.L𝓭_length Dimension.T𝓭_length Dimension.L𝓭_time Dimension.T𝓭_time Dimension.L𝓭_mass Dimension.T𝓭_mass Dimension.L𝓭_charge Dimension.T𝓭_charge Dimension.L𝓭_temperature Dimension.T𝓭_temperature
example1_energyMass 📖	mathematical	—	EnergyMass Dimension.M𝓭 Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 UnitChoices.SI	—	CarriesDimension.toDimensionful_apply_apply LengthUnit.div_self TimeUnit.div_self MassUnit.div_self ChargeUnit.div_self TemperatureUnit.div_self
example2_energyMass 📖	mathematical	—	EnergyMass UnitDependent.scaleUnit WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent UnitChoices.SI Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭	—	UnitChoices.scaleUnit_apply_fst energyMass_isDimensionallyCorrect UnitDependent.scaleUnit_symm_apply example1_energyMass
newtonsSecondWithDim'_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 instUnitDependentForall_1 NewtonsSecondWithDim'	—	WithDim.cast.congr_simp DMul.hMul_scaleUnit WithDim.cast_scaleUnit
newtonsSecondWithDim_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 instUnitDependentForall_1 NewtonsSecondWithDim	—	WithDim.val_mul_eq_mul DMul.hMul_scaleUnit WithDim.scaleUnit_val_eq_scaleUnit_val_of_dim_eq Dimension.ext Dimension.L𝓭_length Dimension.T𝓭_length Dimension.L𝓭_time Dimension.T𝓭_time Dimension.L𝓭_mass Dimension.T𝓭_mass Dimension.L𝓭_charge Dimension.T𝓭_charge Dimension.L𝓭_temperature Dimension.T𝓭_temperature
oddDimensions_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension.M𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent Dimension.Θ𝓭 Dimension Dimension.instCommGroup Dimension.C𝓭 Dimension.T𝓭 Dimension.L𝓭 instUnitDependentForall_1 Dimension.instMul OddDimensions	—	WithDim.cast.congr_simp WithDim.div_scaleUnit DMul.hMul_scaleUnit WithDim.cast_scaleUnit
speedEq_isDimensionallyCorrect 📖	mathematical	—	IsDimensionallyCorrect instUnitDependentTwoSided WithDim Dimension Dimension.instMul Dimension.L𝓭 Dimension.instCommGroup Dimension.T𝓭 MulUnitDependent.toUnitDependent CarriesDimension.toMulAction WithDim.instHasDim WithDim.instMulActionNNReal instMulUnitDependent instUnitDependentForall_1 SpeedEq	—	WithDim.cast.congr_simp WithDim.div_scaleUnit

---

← Back to Index