@[reducible, inline]

abbrev SI.half_frequency_unit : UnitsSystem.Dimensions

Equations

• SI.half_frequency_unit = (1 / 2) • SI.frequency_unit

@[reducible, inline]

abbrev SI.SqrtFrequency : Type

Equations

• SI.SqrtFrequency = UnitsSystem.Scalar SI.half_frequency_unit

@[reducible, inline]

abbrev SI.sqrt_hertz : SqrtFrequency

Equations

• SI.sqrt_hertz = UnitsSystem.StandardUnit SI.half_frequency_unit

@[reducible, inline]

abbrev SI.NNTemperature : Type

An example of a non-negative scalar type

Equations

• SI.NNTemperature = { T : SI.Temperature // T ≥ 0 }