Dimensions of measurement

The base dimensions a measure function measures in (mass, volume, distance, time, cardinality, …) and the dimension group of the quantity calculus they generate: the free abelian group on the base dimensions, written multiplicatively, so that .of .mass / .of .volume is the dimension of density and 1 that of pure numbers.

References

• [scontras-2014]
• [zabbal-2005]
• [de-boer-1995]

inductive Degree.Dimension : Type

A base dimension of measurement. cardinality is the dimension of [zabbal-2005]'s CARD, the Num head behind cardinal numerals, aligned by [scontras-2014] with measure terms.

• mass : Dimension
• volume : Dimension
• distance : Dimension
• time : Dimension
• cardinality : Dimension
• temperature : Dimension
• area : Dimension
• force : Dimension

def Degree.instReprDimension.repr : Dimension → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Degree.instReprDimension.repr Degree.Dimension.mass prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Dimension.mass")).group prec✝
• Degree.instReprDimension.repr Degree.Dimension.volume prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Dimension.volume")).group prec✝
• Degree.instReprDimension.repr Degree.Dimension.distance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Dimension.distance")).group prec✝
• Degree.instReprDimension.repr Degree.Dimension.time prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Dimension.time")).group prec✝
• Degree.instReprDimension.repr Degree.Dimension.area prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Dimension.area")).group prec✝
• Degree.instReprDimension.repr Degree.Dimension.force prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Dimension.force")).group prec✝

@[instance_reducible]

instance Degree.instReprDimension : Repr Dimension

Equations

• Degree.instReprDimension = { reprPrec := Degree.instReprDimension.repr }

@[instance_reducible]

instance Degree.instDecidableEqDimension : DecidableEq Dimension

Equations

• Degree.instDecidableEqDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Degree.instFintypeDimension : Fintype Dimension

Equations

• Degree.instFintypeDimension = { elems := { val := ↑Degree.Dimension.enumList, nodup := Degree.Dimension.enumList_nodup }, complete := Degree.instFintypeDimension._proof_1 }

@[reducible, inline]

abbrev Degree.QuantityDimension : Type

The dimensions of the quantity calculus: the free abelian group on the base dimensions, written multiplicatively.

Equations

• Degree.QuantityDimension = Multiplicative (Degree.Dimension → ℤ)

def Degree.QuantityDimension.of (d : Dimension) : QuantityDimension

The base dimension d as a generator of the dimension group.

Equations

• Degree.QuantityDimension.of d = Multiplicative.ofAdd (Pi.single d 1)

@[simp]

theorem Degree.QuantityDimension.of_ne_one (d : Dimension) : of d ≠ 1

theorem Degree.QuantityDimension.of_injective : Function.Injective of

@[simp]

theorem Degree.QuantityDimension.of_inj {d d' : Dimension} : of d = of d' ↔ d = d'

@[simp]

theorem Degree.QuantityDimension.div_of_ne_self (a : QuantityDimension) (d : Dimension) : a / of d ≠ a

Dividing by a base dimension changes the dimension.