Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Units.WithDim.Basic

Energy

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

@[expose] public section

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

abbrev DimEnergy : Type := Dimensionful (WithDim (M𝓭 * L𝓭 * L𝓭 * T𝓭⁻¹ * T𝓭⁻¹) )