Physlib.Units.WithDim.Basic

Let $d$ be a physical dimension and $M$ be a type. For any two elements $x_1, x_2$ of the type $\text{WithDim}(d, M)$, if their underlying values in $M$ are equal (i.e., $x_1.\text{val} = x_2.\text{val}$), then $x_1 = x_2$.

For any dimension $d$ and any type $M$, the type $\text{WithDim}(d, M)$ is equipped with an instance of the `HasDim` typeclass, which assigns it the physical dimension $d$.

For any physical dimension $d$ and any type $M$, the dimension of the type $\text{WithDim}(d, M)$ is equal to $d$, expressed as $\text{dim}(\text{WithDim}(d, M)) = d$.

Given a physical dimension $d$ and a type $M$ that possesses a scalar action by the non-negative real numbers $\mathbb{R}_{\ge 0}$, the type $\text{WithDim}(d, M)$ (representing values of type $M$ associated with dimension $d$) also inherits a scalar action by $\mathbb{R}_{\ge 0}$. For any scalar $a \in \mathbb{R}_{\ge 0}$ and any dimensioned quantity $m \in \text{WithDim}(d, M)$, the resulting value is obtained by applying the scalar action to the underlying value of $m$.

Let $d$ be a physical dimension and $M$ be a type equipped with a scalar action by the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any scalar $a \in \mathbb{R}_{\ge 0}$ and any dimensioned quantity $m \in \text{WithDim}(d, M)$, the underlying numerical value of the scalar product $a \cdot m$ is equal to the scalar action of $a$ on the numerical value of $m$, expressed as $(a \cdot m).\text{val} = a \cdot m.\text{val}$.

Given two physical dimensions $d_1, d_2 \in \text{Dimension}$, let $m_1$ be a real quantity with dimension $d_1$ (of type $\text{WithDim } d_1 \, \mathbb{R}$) and $m_2$ be a real quantity with dimension $d_2$ (of type $\text{WithDim } d_2 \, \mathbb{R}$). This definition provides the multiplication operation $m_1 \cdot m_2$, which results in a real quantity with the product dimension $d_1 \cdot d_2$. The numerical value of the result is the product of the numerical values of $m_1$ and $m_2$.

Let $d_1$ and $d_2$ be physical dimensions. For any real-valued physical quantities $m_1$ with dimension $d_1$ and $m_2$ with dimension $d_2$, the numerical value of their product $m_1 \cdot m_2$ (which has dimension $d_1 \cdot d_2$) is equal to the product of their individual numerical values. That is, $$(m_1 \cdot m_2).\text{val} = m_1.\text{val} \cdot m_2.\text{val}$$ where the `.val` operator extracts the underlying real number from the dimension-carrying type.

Given two physical dimensions $d_1, d_2 \in \text{Dimension}$, let $m_1$ be a real quantity with dimension $d_1$ (of type $\text{WithDim } d_1 \, \mathbb{R}$) and $m_2$ be a real quantity with dimension $d_2$ (of type $\text{WithDim } d_2 \, \mathbb{R}$). This definition provides the multiplication operation $m_1 \cdot m_2$, which results in a real quantity with the product dimension $d_1 \cdot d_2$. The numerical value of the result corresponds to the product of the numerical values of $m_1$ and $m_2$, while the physical dimension is updated to $d_1 \cdot d_2$.

Let $d_1$ and $d_2$ be physical dimensions. For any real-valued physical quantities $m_1$ with dimension $d_1$ (of type $\text{WithDim } d_1 \, \mathbb{R}$) and $m_2$ with dimension $d_2$ (of type $\text{WithDim } d_2 \, \mathbb{R}$), the product of their numerical values is equal to the numerical value of their physical product: $$m_1.\text{val} \cdot m_2.\text{val} = (m_1 \cdot m_2).\text{val}$$ where $m_1 \cdot m_2$ is the quantity with dimension $d_1 \cdot d_2$ resulting from the multiplication of $m_1$ and $m_2$.

For any physical dimension $d_1$ and any real-valued physical quantity $m_1$ with dimension $d_1$ (of type $\text{WithDim } d_1 \, \mathbb{R}$), the square of the numerical value of $m_1$ is equal to the numerical value of the product of $m_1$ with itself, denoted as $m_1.\text{val}^2 = (m_1 \cdot m_1).\text{val}$.

Let $d$ be a physical dimension and $M$ be a type equipped with a scalar action of the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any two choices of unit systems $u_1, u_2 \in \text{UnitChoices}$ and any two dimensioned quantities $m_1, m_2 \in \text{WithDim}(d, M)$, the numerical values of the quantities after scaling from $u_1$ to $u_2$ are equal if and only if their original numerical values are equal: $$(\text{scaleUnit}(u_1, u_2, m_1)).\text{val} = (\text{scaleUnit}(u_1, u_2, m_2)).\text{val} \iff m_1.\text{val} = m_2.\text{val}$$ Where $\text{WithDim}(d, M)$ denotes the type $M$ carrying the dimension $d$, $m.\text{val}$ is the underlying numerical value of the quantity $m$, and $\text{scaleUnit}$ is the transformation function for transitioning a quantity between unit systems.

Let $d$ be a physical dimension and $M$ be a type equipped with a scalar action by the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any two unit choices $u_1, u_2 \in \text{UnitChoices}$ and any quantity $m_1$ with dimension $d$ (of type $\text{WithDim } d \, M$), the numerical value of the quantity after scaling from unit system $u_1$ to $u_2$ is equal to the scaling factor for dimension $d$ between these unit systems applied to the original numerical value of $m_1$. That is: $$\text{val}(\text{scaleUnit}(u_1, u_2, m_1)) = \text{dimScale}(u_1, u_2, d) \cdot \text{val}(m_1)$$ where $\text{val}(m)$ denotes the underlying value of the dimensioned quantity $m$, and the operation on the right is the scalar action of $\mathbb{R}_{\ge 0}$ on $M$.

For any two physical dimensions $d_1, d_2 \in \text{Dimension}$, the division of a real-valued quantity $m_1$ of dimension $d_1$ by a real-valued quantity $m_2$ of dimension $d_2$ is defined. The resulting quantity $m_1 / m_2$ has the dimension $d_1 \cdot d_2^{-1}$ and its numerical value is the quotient of the values of $m_1$ and $m_2$, namely $\text{val}(m_1 / m_2) = \text{val}(m_1) / \text{val}(m_2)$.

For any physical dimensions $d_1, d_2 \in \text{Dimension}$ and any real-valued quantities $m_1$ with dimension $d_1$ and $m_2$ with dimension $d_2$, the quotient of their numerical values $\text{val}(m_1) / \text{val}(m_2)$ is equal to the numerical value of their dimensional quotient $\text{val}(m_1 / m_2)$. That is: $$\frac{\text{val}(m_1)}{\text{val}(m_2)} = \text{val}\left(\frac{m_1}{m_2}\right)$$ where $\text{val}(m)$ denotes the underlying real value of a quantity $m$ carrying a dimension.

For any physical dimensions $d_1, d_2 \in \text{Dimension}$ and any real-valued quantities $m_1 \in \text{WithDim}(d_1, \mathbb{R})$ and $m_2 \in \text{WithDim}(d_2, \mathbb{R})$, let $u_1, u_2 \in \text{UnitChoices}$ be two systems of units. The division of the quantities after scaling them from unit system $u_1$ to $u_2$ is equal to the result of scaling their quotient from $u_1$ to $u_2$. That is: $$\frac{\text{scaleUnit}(u_1, u_2, m_1)}{\text{scaleUnit}(u_1, u_2, m_2)} = \text{scaleUnit}\left(u_1, u_2, \frac{m_1}{m_2}\right)$$ where $\text{scaleUnit}(u_1, u_2, m)$ denotes the conversion of a quantity $m$ from unit system $u_1$ to $u_2$, and the quotient $m_1 / m_2$ on the right-hand side carries the dimension $d_1 \cdot d_2^{-1}$.

For any dimension $d$ and any type $M$, let $m$ be a quantity of type $M$ carrying the dimension $d$. Casting $m$ to the same dimension $d$ (using the reflexivity of equality $d = d$) results in the original quantity $m$. That is, $\text{cast } m \text{ rfl} = m$.

Let $d$ and $d_2$ be physical dimensions, and let $M$ be a type equipped with a scalar action of the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any quantity $m \in \text{WithDim}(d, M)$ and any two unit systems $u_1, u_2 \in \text{UnitChoices}$, if $d = d_2$ (denoted by the proof $h$), then casting the scaled quantity to dimension $d_2$ is equivalent to scaling the quantity after it has been cast to dimension $d_2$. That is, $$\text{cast}(\text{scaleUnit}(u_1, u_2, m), h) = \text{scaleUnit}(u_1, u_2, \text{cast}(m, h)).$$

For any physical dimension $d$ and any type $M$ that forms an additive commutative group, the type $\text{WithDim}(d, M)$ (representing values of type $M$ carrying the dimension $d$) also forms an additive commutative group. The group operations, such as addition, negation, and the zero element, are inherited from the underlying operations of $M$.

For any physical dimension $d$ and any type $M$ equipped with a less-than-or-equal-to relation $\le$, the type $\text{WithDim}(d, M)$ (which represents values of type $M$ carrying the dimension $d$) also possesses a less-than-or-equal-to relation $\le$. This relation is inherited from $M$, meaning for any $m_1, m_2 \in \text{WithDim}(d, M)$, $m_1 \le m_2$ holds if and only if their underlying values in $M$ satisfy the relation.

For any physical dimension $d$ and any type $M$ equipped with a less-than-or-equal-to relation $\le$, let $m_1$ and $m_2$ be elements of the type $\text{WithDim}(d, M)$, which represents values of type $M$ carrying the dimension $d$. Then $m_1 \le m_2$ holds if and only if their underlying values in $M$ satisfy $m_1.\text{val} \le m_2.\text{val}$.

Given a dimension $d$ and a type $M$ equipped with a strict inequality relation $<$, this instance defines the strict inequality relation for the type $\text{WithDim} \ d \ M$. For any two elements $m_1, m_2 \in \text{WithDim} \ d \ M$, the relation $m_1 < m_2$ holds if and only if their underlying values satisfy the relation $m_1.\text{val} < m_2.\text{val}$ in $M$.

Let $d$ be a dimension and $M$ be a type equipped with a strict inequality relation $<$. For any elements $m_1, m_2$ of type $\text{WithDim} \ d \ M$, the relation $m_1 < m_2$ holds if and only if their underlying values satisfy $m_1.\text{val} < m_2.\text{val}$ in $M$.

For any physical dimension $d$ and any type $M$ equipped with a preorder structure, the type $\text{WithDim}(d, M)$ (representing values of type $M$ carrying the dimension $d$) also forms a preorder. This structure is inherited from $M$, where the relations $\le$ and $<$ between two elements $m_1, m_2 \in \text{WithDim}(d, M)$ are defined by the relations between their underlying values in $M$.

For any physical dimension $d$ and any type $M$ equipped with a partial order structure, the type $\text{WithDim}(d, M)$ (representing values of type $M$ carrying the dimension $d$) also forms a partial order. This structure is inherited from $M$, where the relations $\le$ and $<$ between two elements $m_1, m_2 \in \text{WithDim}(d, M)$ are defined by the corresponding relations between their underlying values $m_1.\text{val}$ and $m_2.\text{val}$ in $M$.

For a given dimension basis $B$ and a dimension $d \in \text{Dimension } B$, let $M$ be a type that possesses a module structure over the real numbers $\mathbb{R}$ (such as $\mathbb{R}$ itself or a vector space). The type $\text{WithDim } d \, M$ represents elements of $M$ that are tagged with the physical dimension $d$. This definition establishes that $\text{WithDim } d \, M$ is also a module over $\mathbb{R}$, where a dimensionless real scalar $r \in \mathbb{R}$ acts on a dimension-tagged quantity $x$ by scaling its underlying numerical value in $M$.

Let $B$ be a dimension basis, $d$ be a dimension in that basis, and $M$ be an $\mathbb{R}$-module. For any real scalar $r \in \mathbb{R}$ and any quantity $x \in \text{WithDim } d \, M$, the underlying value of the scalar product $r \cdot x$ is equal to the scalar product of $r$ and the underlying value of $x$. That is, $(r \cdot x).\text{val} = r \cdot x.\text{val}$.

For physical dimensions $d_1, d_2$ defined over the default base dimensions ($L, T, M, C, \Theta$), this instance defines the multiplication of two real quantities carrying these dimensions. Given a quantity $x$ of type $\text{WithDim } d_1 \, \mathbb{R}$ and a quantity $y$ of type $\text{WithDim } d_2 \, \mathbb{R}$, their product $x \cdot y$ results in a real quantity with the product dimension $d_1 \cdot d_2$, specifically of type $\text{WithDim } (d_1 \cdot d_2) \, \mathbb{R}$.