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

Pressure

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

@[expose] public section

Pressure as a dimensional quantity with dimension ML⁻¹T⁻2..

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