def Units.«commandDef_base_dimension_:=_» : Lean.ParserDescr

Define a base dimension.

Example:

• def_base_dimension Length := "L"

Equations

• One or more equations did not get rendered due to their size.

def Units.«commandDef_derived_dimension_:=_» : Lean.ParserDescr

Define a derived dimension.

Example:

• def_derived_dimension Area := Length^2

Equations

• One or more equations did not get rendered due to their size.

def Units.«commandDef_base_unit_:=_From_» : Lean.ParserDescr

Define a base unit.

Example:

• def_base_unit meter := "m" from Dimension.Length

Equations

• One or more equations did not get rendered due to their size.

def Units.«commandDef_derived_unit_:=_From_» : Lean.ParserDescr

Define a derived unit.

Example:

• def_derived_unit newton := "N" from kilogram * meter / second^2

Equations

• One or more equations did not get rendered due to their size.

def Units.«commandDef_derived_unit_:=_From_With_» : Lean.ParserDescr

Define a derived unit with conversion.

Example:

• def_derived_unit celsius := "°C" from kelvin with Conversion.translate (27315/100)

Equations

• One or more equations did not get rendered due to their size.