structure Units.Dimension : Type

A dimension is a product of base dimensions raised to rational powers. For example, the dimension of force in the SI system is Mass•Length•Time⁻² can be represented as :

• force = {"Mass" ↦ 1, "Length" ↦ 1, "Time" ↦ -2} you build it by combining base dimensions using multiplication and division.
• To build a base dimension, use the helper macro def_base_dimension Length := "L"
• To build a derived dimension, use multiplication *, division / and exponentiation ^.

For example, the dimension of Area can be built using the helper macro:

• def_derived_dimension Area := Length^2

Note that using macros is encouraged to ensure correct simplification of dimensions when casting.

• _impl : Π₀ (x : String), ℚ

theorem Units.Dimension.ext_iff {x y : Dimension} : x = y ↔ x._impl = y._impl

theorem Units.Dimension.ext {x y : Dimension} (_impl : x._impl = y._impl) : x = y

def Units.instDecidableEqDimension.decEq (x✝ x✝¹ : Dimension) : Decidable (x✝ = x✝¹)

Equations

• Units.instDecidableEqDimension.decEq { _impl := a } { _impl := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Units.instDecidableEqDimension : DecidableEq Dimension

Equations

• Units.instDecidableEqDimension = Units.instDecidableEqDimension.decEq

def Units.instBEqDimension.beq : Dimension → Dimension → Bool

Equations

• Units.instBEqDimension.beq { _impl := a } { _impl := b } = (a == b)
• Units.instBEqDimension.beq x✝¹ x✝ = false

instance Units.instBEqDimension : BEq Dimension

Equations

• Units.instBEqDimension = { beq := Units.instBEqDimension.beq }

class Units.HasDimension (μ : Type) : Type

A typeclass for types that have an associated dimension.

• dimension (u : μ) : Dimension

def Units.𝒟 {μ : Type} [self : HasDimension μ] (u : μ) : Dimension

Alias of Units.HasDimension.dimension.

Equations

• @Units.𝒟 = @Units.HasDimension.dimension

def Units.Dimension.ofString (s : String) : Dimension

Create a dimension from a string identifier. Each unique string represents a different fundamental dimension. For example, "L" for Length, "M" for Mass, "T" for Time, etc.

Equations

• Units.Dimension.ofString s = { _impl := fun₀ | s => 1 }

def Units.Dimension.dimensionless : Dimension

The dimension with no fundamental dimensions, representing a dimensionless quantity.

Equations

• Units.Dimension.dimensionless = { _impl := 0 }

def Units.Dimension.IsBase (d : Dimension) : Prop

A dimension is a base dimension if it corresponds to a single fundamental dimension, represented by a string identifier and has an exponent of 1.

Equations

• d.IsBase = ∃ (s : String), d = Units.Dimension.ofString s

def Units.Dimension.bases (d : Dimension) : List String

Equations

• d.bases = Units.Dimension.bases.unsafe_impl_3 d

def Units.Dimension.IsBase' (d : Dimension) : Bool

Equations

• d.IsBase' = match d.bases with | [s] => d._impl s == 1 | x => false

def Units.Dimension.base_name (d : Dimension) (h : d.IsBase' = true) : String

Equations

• d.base_name h = d.bases.head ⋯

def Units.Dimension.IsSingle (d : Dimension) : Prop

A dimension is a single dimension if it corresponds to a single fundamental dimension, represented by a string identifier and a rational exponent.

Equations

• d.IsSingle = ∃ (s : String) (q : ℚ), q ≠ 0 ∧ d = { _impl := fun₀ | s => q }

noncomputable def Units.Dimension.IsBase.name {d : Dimension} (h : d.IsBase) : String

Non computable function to extract the name of the base dimension.

Equations

• h.name = Classical.choose h

def Units.Dimension.IsBase.exponent {d : Dimension} : d.IsBase → ℚ

Equations

• x✝.exponent = 1

theorem Units.Dimension.IsBase.name_spec {d : Dimension} (h : d.IsBase) : d = ofString h.name

The specification that the name corresponds to the base dimension.

theorem Units.Dimension.IsBase.name_exponent_spec {d : Dimension} (h : d.IsBase) : h.exponent = 1 ∧ d = { _impl := fun₀ | h.name => h.exponent }

The specification that the name and exponent correspond to the base dimension.

noncomputable def Units.Dimension.IsSingle.name {d : Dimension} (h : d.IsSingle) : String

Non computable function to extract the name and exponent of the single dimension.

ie: dimensions like Length^2 or Time^-1

Equations

• h.name = Classical.choose h

noncomputable def Units.Dimension.IsSingle.exponent {d : Dimension} (h : d.IsSingle) : ℚ

Non computable function to extract the exponent of the single dimension.

ie: dimensions like Length^2 or Time^-1

Equations

• h.exponent = Classical.choose ⋯

theorem Units.Dimension.IsSingle.name_exponent_spec {d : Dimension} (h : d.IsSingle) : h.exponent ≠ 0 ∧ d = { _impl := fun₀ | h.name => h.exponent }

The specification that the name and exponent correspond to the single dimension.

def Units.Dimension.DecidableNEqZero (α : Type u) [Zero α] : Type u

Equations

• Units.Dimension.DecidableNEqZero α = ((x : α) → Decidable (x ≠ 0))

instance Units.Dimension.instAddCommGroup : AddCommGroup Dimension

Equations

• Units.Dimension.instAddCommGroup = Units.Dimension.instEquiv.addCommGroup

instance Units.Dimension.instSMul : SMul ℚ Dimension

Equations

• Units.Dimension.instSMul = Equiv.smul ℚ Units.Dimension.instEquiv

instance Units.Dimension.instMulAction : MulAction ℚ Dimension

Equations

• Units.Dimension.instMulAction = { toSMul := Units.Dimension.instSMul, one_smul := Units.Dimension.instMulAction._proof_1, mul_smul := Units.Dimension.instMulAction._proof_2 }

instance Units.Dimension.instSMulWithZero : SMulWithZero ℚ Dimension

Equations

• Units.Dimension.instSMulWithZero = { toSMul := Units.Dimension.instSMul, smul_zero := Units.Dimension.instSMulWithZero._proof_1, zero_smul := Units.Dimension.instSMulWithZero._proof_2 }

instance Units.Dimension.instModule : Module ℚ Dimension

Equations

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

instance Units.Dimension.instHasDimension : HasDimension Dimension

Equations

• Units.Dimension.instHasDimension = { dimension := fun (u : Units.Dimension) => u }

instance Units.Dimension.instSetoidUnit : Setoid Dimension

Equations

• Units.Dimension.instSetoidUnit = { r := fun (x1 x2 : Units.Dimension) => x1 = x2, iseqv := Units.Dimension.instSetoidUnit._proof_1 }

instance Units.Dimension.instDecidableEquivDimension (a b : Dimension) : Decidable (a ≈ b)

Equations

• a.instDecidableEquivDimension b = id inferInstance

instance Units.Dimension.instOne : One Dimension

Equations

• Units.Dimension.instOne = { one := 0 }

instance Units.Dimension.instMul : Mul Dimension

Equations

• Units.Dimension.instMul = { mul := fun (u1 u2 : Units.Dimension) => u1 + u2 }

instance Units.Dimension.instInv : Inv Dimension

Equations

• Units.Dimension.instInv = { inv := fun (u : Units.Dimension) => -u }

instance Units.Dimension.instDiv : Div Dimension

Equations

• Units.Dimension.instDiv = { div := fun (u1 u2 : Units.Dimension) => u1 - u2 }

instance Units.Dimension.instPowNat : Pow Dimension ℕ

Equations

• Units.Dimension.instPowNat = { pow := fun (u : Units.Dimension) (q : ℕ) => q • u }

instance Units.Dimension.instPowInt : Pow Dimension ℤ

Equations

• Units.Dimension.instPowInt = { pow := fun (u : Units.Dimension) (n : ℤ) => n • u }

instance Units.Dimension.instPowRat : Pow Dimension ℚ

Equations

• Units.Dimension.instPowRat = { pow := fun (u : Units.Dimension) (n : ℚ) => n • u }

noncomputable def Units.Dimension.PrimeScale (d : Dimension) : ℝ

Equations

• d.PrimeScale = d._impl.prod Units.Dimension.PrimeScale.prime_pow

noncomputable def Units.Dimension.OneScale : Dimension → ℝ

Equations

• x✝.OneScale = 1

instance Units.Dimension.instRepr : Repr Dimension

Equations

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

instance Units.Dimension.instToString : ToString Dimension

Equations

• Units.Dimension.instToString = { toString := fun (d : Units.Dimension) => reprStr d }