Energy

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

@[reducible, inline]

abbrev DimEnergy : Type

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

noncomputable def DimEnergy.joule : DimEnergy

The dimensional energy corresponding to 1 joule, J.

noncomputable def DimEnergy.electronVolt : DimEnergy

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

noncomputable def DimEnergy.calorie : DimEnergy

The dimensional energy corresponding to 1 calorie, 4.184 J.

noncomputable def DimEnergy.kilowattHour : DimEnergy

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