Physlib.ClassicalMechanics.Mass.MassUnit

For any mass unit $x$, its associated numerical value $x.\text{val}$ is non-zero. In the context of `Physlib`, a `MassUnit` is defined as being equivalent to the positive real numbers $\mathbb{R}_{>0}$, and $x.\text{val}$ represents the real number associated with that unit.

For any mass unit $x$, its associated numerical value $x.\text{val}$ is strictly positive ($x.\text{val} > 0$). In the context of `Physlib`, a `MassUnit` is defined as being equivalent to the positive real numbers $\mathbb{R}_{>0}$, and $x.\text{val}$ represents the real number associated with that unit.

The type `MassUnit` is provided with a default element, specified as the unit whose underlying numerical value is $1$. In the context of this library, this default element represents the kilogram.

The division operation for mass units $x$ and $y$ is defined such that their ratio $x / y$ is a non-negative real number $\mathbb{R}_{\geq 0}$, calculated as the quotient of their underlying numerical values $\frac{x.\text{val}}{y.\text{val}}$.

For any two mass units $x$ and $y$, their ratio $x / y$ is equal to the quotient of their underlying numerical values $\frac{x.\text{val}}{y.\text{val}}$ as a non-negative real number in $\mathbb{R}_{\geq 0}$.

For any two mass units $x$ and $y$, the ratio of $x$ to $y$ is non-zero. That is, $x / y \neq 0$ where the result is a non-negative real number in $\mathbb{R}_{\geq 0}$.

For any two mass units $x$ and $y$, the ratio of $x$ to $y$ is strictly positive. That is, $0 < x / y$ where the result is a non-negative real number in $\mathbb{R}_{\geq 0}$.

For any mass unit $x$, the ratio of $x$ to itself is equal to $1$. That is, $x / x = 1$ where the result is a non-negative real number $\mathbb{R}_{\geq 0}$.

For any two mass units $x$ and $y$, the ratio of $x$ to $y$ is equal to the reciprocal (multiplicative inverse) of the ratio of $y$ to $x$. That is, $x / y = (y / x)^{-1}$, where the division $a / b$ represents the non-negative real ratio between two mass units in $\mathbb{R}_{\geq 0}$.

For any three mass units $x$, $y$, and $z$, the product of the ratio of $x$ to $y$ and the ratio of $y$ to $z$ is equal to the ratio of $x$ to $z$. That is, $(x / y) \cdot (y / z) = x / z$, where the division $a / b$ represents the non-negative real ratio between two mass units.

For any mass unit $x$ and any positive real number $r > 0$, let $\text{scale}(r, x)$ denote the mass unit $x$ scaled by the factor $r$. The ratio of this scaled unit to the original unit $x$ is equal to $r$. That is, $\text{scale}(r, x) / x = r$, where the division represents the non-negative real ratio between the two mass units.

For any mass unit $x$ and any positive real number $r > 0$, the ratio of the unit $x$ to the unit $x$ scaled by $r$ (denoted $\text{scale}(r, x)$) is equal to $1/r$. Here, the division $x / y$ of two mass units represents their ratio as a non-negative real number in $\mathbb{R}_{\geq 0}$.

For any mass unit $x$, the result of scaling $x$ by the factor $1$ is equal to $x$.

For any two mass units $x_1, x_2 \in \text{MassUnit}$ and any positive real numbers $r_1, r_2 \in \mathbb{R}$ (where $r_1, r_2 > 0$), the ratio of the scaled units satisfies the identity: $$\frac{\text{scale}(r_1, x_1)}{\text{scale}(r_2, x_2)} = \frac{r_1}{r_2} \cdot \frac{x_1}{x_2}$$ where $\text{scale}(r, x)$ denotes the unit $x$ scaled by the factor $r$, and the division $a/b$ of two mass units represents their ratio as a non-negative real number in $\mathbb{R}_{\geq 0}$.

For any mass unit $x \in \text{MassUnit}$ and any positive real numbers $r_1, r_2 \in \mathbb{R}$ (where $r_1 > 0$ and $r_2 > 0$), scaling the unit $x$ by $r_2$ and then scaling the resulting unit by $r_1$ is equivalent to scaling the original unit $x$ by the product $r_1 \cdot r_2$: $$\text{scale}(r_1, \text{scale}(r_2, x)) = \text{scale}(r_1 \cdot r_2, x)$$ where $\text{scale}(r, x)$ denotes the mass unit $x$ scaled by the factor $r$.

The kilogram is defined as the unit of mass corresponding to the value $1$ in the type `MassUnit`, which is represented by the set of positive real numbers $\mathbb{R}_{>0}$. This choice serves as the reference scale for all other mass units.

The mass unit of micrograms is defined as $10^{-9}$ times the mass unit of kilograms. In the `MassUnit` type, which is represented by the positive real numbers $\mathbb{R}_{>0}$ where kilograms is the reference unit (value 1), a microgram corresponds to the element obtained by scaling the kilogram unit by a factor of $(1/10)^9 = 10^{-9}$.

The mass unit of milligrams is defined as $10^{-6}$ times the mass unit of kilograms. In the `MassUnit` type, which is modeled by the positive real numbers $\mathbb{R}_{>0}$ with kilograms as the reference unit (value 1), a milligram is the element obtained by scaling the kilogram unit by a factor of $(1/10)^6$.

The mass unit of grams is defined as $10^{-3}$ times the mass unit of kilograms. Specifically, in the `MassUnit` type, a gram is the element obtained by scaling the reference unit of kilograms by a factor of $(1/10)^3 = 10^{-3}$.

The mass unit of (avoirdupois) ounces is defined as $0.028349523125$ times the mass unit of kilograms. Specifically, in the `MassUnit` type (which is represented by the set of positive real numbers $\mathbb{R}_{>0}$ where kilograms serve as the reference unit with value $1$), an ounce is the element obtained by scaling the kilogram unit by the factor $0.028349523125$.

The mass unit of (avoirdupois) pounds is defined as $0.45359237$ times the mass unit of kilograms. Specifically, in the `MassUnit` type (which is represented by the set of positive real numbers $\mathbb{R}_{>0}$), a pound is the element obtained by scaling the reference unit of kilograms by the factor $0.45359237$.

The mass unit of stones is defined as $14$ times the mass unit of pounds. Specifically, in the `MassUnit` type (which is represented by the set of positive real numbers $\mathbb{R}_{>0}$), a stone is the element obtained by scaling the previously defined unit of pounds by a factor of $14$.

The mass unit of quarters is defined as $28$ times the mass unit of pounds. Specifically, within the `MassUnit` type (which is identified with the set of positive real numbers $\mathbb{R}_{>0}$), a quarter is the element obtained by scaling the value of a pound by a factor of $28$.

The mass unit of hundredweights is defined as $112$ times the mass unit of pounds. Within the `MassUnit` type, which is represented by the set of positive real numbers $\mathbb{R}_{>0}$, the hundredweight is the element obtained by scaling the unit of pounds by a factor of $112$.

The short ton is a unit of mass defined as 2000 times the value of the mass unit of pounds. Within the `MassUnit` framework, where mass units are represented by the set of positive real numbers $\mathbb{R}_{>0}$ relative to a reference kilogram, the short ton corresponds to the element obtained by scaling the unit of pounds by a factor of $2000$.

The metric ton is defined as the unit of mass obtained by scaling the reference unit of kilograms by a factor of $1000$.

The mass unit of long tons is defined as $2240$ times the mass unit of pounds. In the `MassUnit` type, which is represented by the set of positive real numbers $\mathbb{R}_{>0}$, a long ton (also known as a shortweight ton) is the element obtained by scaling the unit of pounds by a factor of $2240$.

The nominal solar mass unit is defined as the unit of mass obtained by scaling the reference unit of kilograms by a factor of $1.988416 \times 10^{30}$.

The ratio of the mass unit of pounds to the mass unit of ounces is equal to $16$. Formally, $\text{pounds} / \text{ounces} = 16$, where the division of these two mass units results in a non-negative real number $\mathbb{R}_{\geq 0}$.

The ratio of the mass unit of short tons to the mass unit of kilograms is equal to $907.18474$. Formally, $\text{shortTons} / \text{kilograms} = 907.18474$, where the division of these two mass units results in a non-negative real number $\mathbb{R}_{\geq 0}$ representing the numerical scale of short tons relative to the reference unit of kilograms.

The ratio of the mass unit of long tons to the mass unit of kilograms is equal to $1016.0469088$. Formally, $\text{longTons} / \text{kilograms} = 1016.0469088$, where the division of these two mass units results in a non-negative real number $\mathbb{R}_{\geq 0}$.