Energy

In this module we define the dimensionful type corresponding to an energy. We define specific insances of energy.

@[reducible, inline]

abbrev DimEnergy : Type

Energy as a dimensional quantity with dimension MLT⁻2..

Equations

• DimEnergy = Dimensionful (WithDim (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹ * Dimension.T𝓭⁻¹) ℝ)

noncomputable def DimEnergy.joule : DimEnergy

The dimensional energy corresponding to 1 joule, J.

Equations

• DimEnergy.joule = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 1 }

noncomputable def DimEnergy.electronVolt : DimEnergy

The dimensional energy corresponding to 1 electron volt, 1.602176634×10−19 J.

Equations

• DimEnergy.electronVolt = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 1602176634e-28 }

noncomputable def DimEnergy.calorie : DimEnergy

The dimensional energy corresponding to 1 calorie, 4.184 J.

Equations

• DimEnergy.calorie = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 4.184 }

noncomputable def DimEnergy.kilowattHour : DimEnergy

The dimensional energy corresponding to 1 kilowatt-hours, (3,600,000 J).

Equations

• DimEnergy.kilowattHour = (CarriesDimension.toDimensionful UnitChoices.SI) { val := 3600000 }