Physlib.SpaceAndTime.Space.LengthUnit

For any length unit $x$, its underlying numerical value $x.\text{val}$ is not equal to $0$.

For any length unit $x \in \text{LengthUnit}$, its underlying numerical value $x.\text{val}$ is strictly positive, satisfying $x.\text{val} > 0$.

The type $\text{LengthUnit}$, representing the set of physical length units (isomorphic to the positive real numbers $\mathbb{R}_{>0}$), is inhabited. A default instance is provided, which is defined as the length unit with the underlying value $1$.

The division operation $x / y$ for two length units $x, y \in \text{LengthUnit}$ is defined as the ratio of their underlying values $x.\text{val} / y.\text{val}$, yielding a non-negative real number in $\mathbb{R}_{\geq 0}$.

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

For any length units $x, y \in \text{LengthUnit}$, the ratio $x / y$ is not equal to $0$ in the non-negative real numbers $\mathbb{R}_{\geq 0}$.

For any length units $x, y \in \text{LengthUnit}$, the ratio $x / y$ is strictly greater than $0$ in the non-negative real numbers $\mathbb{R}_{\geq 0}$.

For any length unit $x$, the ratio of $x$ to itself, denoted by $x / x$, is equal to $1$ in the non-negative real numbers $\mathbb{R}_{\geq 0}$.

For any length units $x, y \in \text{LengthUnit}$, the ratio of $x$ to $y$ is equal to the reciprocal of the ratio of $y$ to $x$. Mathematically, this is expressed as: $$x / y = (y / x)^{-1}$$ where the division $a / b$ denotes the ratio of the underlying numerical values of the length units, resulting in a non-negative real number in $\mathbb{R}_{\geq 0}$.

For any length 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$. Mathematically, this is expressed as $(x / y) \cdot (y / z) = x / z$, where the division $a / b$ denotes the ratio of the underlying scales of the length units, treated here as real numbers.

For any length unit $x \in \text{LengthUnit}$ and any positive real number $r \in \mathbb{R}$ (where $r > 0$), the ratio of the unit $x$ scaled by $r$ to the original unit $x$ is equal to $r$. Mathematically, this is expressed as: $$\text{scale}(r, x) / x = r$$ where the division $a / b$ denotes the ratio of the underlying scales of the length units, resulting in a non-negative real number $r \in \mathbb{R}_{\geq 0}$.

Let $x$ be a length unit (an element of `LengthUnit`) and $r$ be a positive real number ($r > 0$). The ratio of the length unit $x$ to the scaled unit $\text{scale}(r, x)$ is equal to the reciprocal of the scaling factor, $1/r$: $$\frac{x}{\text{scale}(r, x)} = 1/r$$ In this expression, the division of length units and the resulting value $1/r$ are treated as non-negative real numbers in $\mathbb{R}_{\geq 0}$.

Let $x$ be a length unit (an element of `LengthUnit`, which corresponds to the set of positive real numbers $\mathbb{R}_{>0}$). Scaling the length unit $x$ by a factor of $1$ results in the original unit $x$: $$\text{scale}(1, x) = x$$

Let $x_1$ and $x_2$ be length units (elements of `LengthUnit`, which corresponds to the set of positive real numbers $\mathbb{R}_{>0}$). For any two positive real numbers $r_1, r_2 \in \mathbb{R}$ such that $r_1 > 0$ and $r_2 > 0$, the ratio of the scaled unit $\text{scale}(r_1, x_1)$ to the scaled unit $\text{scale}(r_2, x_2)$ is equal to the product of the ratio of the scaling factors $r_1/r_2$ and the ratio of the original units $x_1/x_2$: $$\frac{\text{scale}(r_1, x_1)}{\text{scale}(r_2, x_2)} = \left(\frac{r_1}{r_2}\right) \cdot \left(\frac{x_1}{x_2}\right)$$ Here, the division of length units and the scaling factors are treated as non-negative real numbers in $\mathbb{R}_{\geq 0}$.

Let $x$ be a length unit (an element of `LengthUnit`, which corresponds to the set of positive real numbers $\mathbb{R}_{>0}$). For any two positive real numbers $r_1, r_2 \in \mathbb{R}$ such that $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)$$

The length unit "meters" is defined as the element of the type `LengthUnit` (which represents the set of positive real numbers $\mathbb{R}_{>0}$) that corresponds to the value $1$. This serves as the base reference unit from which other length units are scaled.

The length unit "femtometers" is defined as an element of the type `LengthUnit`, which represents the set of positive real numbers $\mathbb{R}_{>0}$. It is obtained by scaling the base unit `meters` by a factor of $10^{-15}$. In the underlying representation where one meter is assigned the value $1$, a femtometer corresponds to the value $10^{-15}$.

The length unit "picometers" is defined as an element of the type `LengthUnit`, which represents the set of positive real numbers $\mathbb{R}_{>0}$. It is obtained by scaling the base unit `meters` by a factor of $10^{-12}$. In the underlying representation where one meter is assigned the value $1$, a picometer corresponds to the value $10^{-12}$.

The length unit "nanometers" is defined as an element of the type `LengthUnit`, which represents the set of positive real numbers $\mathbb{R}_{>0}$. It is obtained by scaling the base unit `meters` by a factor of $10^{-9}$. In the underlying representation where one meter is assigned the value $1$, a nanometer corresponds to the value $10^{-9}$.

The length unit "micrometers" is an element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) defined by scaling the base unit `meters` by a factor of $10^{-6}$. It corresponds to the value $10^{-6}$ in the underlying representation where `meters` is assigned the value $1$.

The length unit "millimeters" is an element of the type `LengthUnit` (which represents the set of positive real numbers $\mathbb{R}_{>0}$) defined by scaling the base unit `meters` by a factor of $10^{-3}$. It corresponds to the value $10^{-3}$ in the underlying representation where one meter is assigned the value $1$.

The length unit "centimeters" is an element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) defined by scaling the base unit `meters` by a factor of $(1/10)^2$, or $10^{-2}$. It corresponds to the value $10^{-2}$ in the underlying representation where `meters` is assigned the value $1$.

The length unit "inches" is an element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) defined by scaling the base unit `meters` by a factor of $0.0254$. It corresponds to the value $0.0254$ in the underlying representation where `meters` is assigned the value $1$.

The length unit "links" is defined as an element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the base unit "meters" by a factor of $0.201168$.

The length unit "feet" is defined as an element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the base unit "meters" by a factor of $0.3048$. In the underlying representation where "meters" corresponds to the value $1$, "feet" corresponds to the value $0.3048$.

The length unit "yards" is defined as an element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the base unit "meters" by a factor of $0.9144$.

The length unit "rods" is defined as the element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the reference unit "meters" by a factor of $5.0292$. In the underlying representation of length units as positive reals, this corresponds to the value $5.0292$.

The length unit "chains" is defined as the element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the reference unit "meters" by a factor of $20.1168$. In the underlying representation where "meters" corresponds to $1$, "chains" corresponds to the value $20.1168$.

The length unit "furlongs" is defined as the element of the type `LengthUnit` (which represents the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the reference unit "meters" by a factor of $201.168$. In the underlying representation of length units as positive reals, this corresponds to the value $201.168$.

The length unit "kilometers" is defined as the element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the reference unit "meters" by a factor of $10^3$. In the underlying representation where "meters" corresponds to $1$, "kilometers" corresponds to the value $1000$.

The length unit "miles" is defined as the element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the reference unit "meters" by a factor of $1609.344$. In the underlying representation where "meters" corresponds to the value $1$, "miles" corresponds to the value $1609.344$.

The length unit "nautical miles" is defined as the element of the type `LengthUnit` (representing the set of positive real numbers $\mathbb{R}_{>0}$) obtained by scaling the reference unit "meters" by a factor of $1852$. In the underlying representation where "meters" corresponds to the value $1$, "nautical miles" corresponds to the value $1852$.

The length unit "astronomical units" is defined as the scaling of the base unit "meters" by a factor of $149,597,870,700$. Within the `LengthUnit` type, which represents the set of positive real numbers $\mathbb{R}_{>0}$ (where "meters" corresponds to the value $1$), this unit corresponds to the value $149,597,870,700$.

The length unit "light years" is defined as the scaling of the base unit "meters" by a factor of $9,460,730,472,580,800$. Within the `LengthUnit` type, which represents positive real numbers $\mathbb{R}_{>0}$, this unit corresponds to the value $9,460,730,472,580,800$.

The length unit "parsecs" is defined as the scaling of the unit "astronomical units" by a factor of $\frac{648,000}{\pi}$. Within the `LengthUnit` type, which represents the set of positive real numbers $\mathbb{R}_{>0}$ (where the unit "meters" corresponds to the value $1$), this unit represents the value of a parsec relative to the base meter, calculated by multiplying the value of an astronomical unit ($149,597,870,700$) by $\frac{648,000}{\pi}$.

The ratio of the length unit `miles` to the length unit `yards` is equal to $1760$ in the non-negative real numbers $\mathbb{R}_{\geq 0}$. This represents the fact that there are exactly 1760 yards in a mile.

There are exactly 220 yards in a furlong. Formally, the ratio of the length unit "furlongs" to the length unit "yards" is equal to the non-negative real number 220, denoted as $\text{furlongs} / \text{yards} = 220$.