Physlib.Units.PositiveRealUnit

For a unit type $U$ equipped with the `PositiveRealUnitCore` structure, this instance provides a default element by defining it as the unit whose magnitude is $1$.

For any unit $x$ of type $U$, its magnitude $\text{val}(x)$ is non-zero.

For two units $x$ and $y$ of the same type $U$, the ratio is defined as the quotient of their magnitudes $\frac{\text{val}(x)}{\text{val}(y)}$, returning a non-negative real number in $\mathbb{R}_{\ge 0}$.

For two units $x$ and $y$ of the same type $U$, the division operation $x / y$ is defined as the ratio of their magnitudes $\frac{\text{val}(x)}{\text{val}(y)}$, resulting in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any two units $x$ and $y$ belonging to a unit type $U$ defined under `PositiveRealUnitCore`, the result of the division $x / y$ is equal to the ratio of their magnitudes $\frac{\text{val}(x)}{\text{val}(y)}$, represented as a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any two units $x$ and $y$ of a positive real unit type $U$, the ratio $x / y$ is strictly greater than $0$ in the set of non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any two units $x$ and $y$ belonging to a positive real unit type $U$, the ratio $x / y$ is not equal to $0$ in the set of non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any unit $x$ of type $U$, the ratio of the unit with itself is equal to the non-negative real number $1$, i.e., $x / x = 1$.

For any two units $x$ and $y$ of the same unit type $U$, the ratio of their magnitudes $x / y$ is equal to the multiplicative inverse of the ratio $y / x$ in the non-negative real numbers $\mathbb{R}_{\ge 0}$, such that $x / y = (y / x)^{-1}$.

For any units $x, y,$ and $z$ of the same positive-real unit type $U$, 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$ in the non-negative real numbers $\mathbb{R}_{\ge 0}$. That is: $$(x / y) \cdot (y / z) = x / z$$ where $x / y$ denotes the ratio of the magnitudes of units $x$ and $y$.

Let $U$ be a positive-real unit type. For any units $x, y, z \in U$, 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$, where these ratios are treated as real numbers: $$(x / y) \cdot (y / z) = x / z$$

Let $U$ be a positive-real unit type. For any unit $x \in U$, any real number $r \in \mathbb{R}$, and a proof $h_r$ that $r > 0$, the numerical magnitude of the rescaled unit is given by the product of the scalar and the original magnitude: $\text{val}(\text{scale}(r, x, h_r)) = r \cdot \text{val}(x)$.

Let $U$ be a positive-real unit type. For any two units $x, y \in U$, if their numerical magnitudes are equal, denoted by $\text{val}(x) = \text{val}(y)$, then the units themselves are equal, $x = y$.

Let $U$ be a positive-real unit type. For any unit $x \in U$ and any real number $r > 0$, the ratio of the rescaled unit to the original unit is equal to the scaling factor $r$, expressed as $\frac{\text{scale}(r, x)}{x} = r$. Here, the division of units of the same type results in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any unit $x$ of a positive-real unit type $U$ and any positive real number $r > 0$, the ratio of the unit $x$ to the unit rescaled by $r$ is equal to the reciprocal of the scaling factor, i.e., $x / \text{scale}(r, x) = 1/r$. Here, the division $x / y$ represents the ratio of the magnitudes of the units in the non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any unit $x$ of type $U$ within the `PositiveRealUnitCore` framework, scaling $x$ by the real number $1$ leaves the unit unchanged, i.e., $\text{scale}(1, x) = x$.

For any units $x_1, x_2$ of type $U$ and any positive real numbers $r_1, r_2 > 0$, rescaling these units by the factors $r_1$ and $r_2$ respectively results in a ratio equal to the ratio of the factors multiplied by the ratio of the original units: $$\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 $x / y$ denotes the ratio of the magnitudes of the units.

For any unit magnitude $x$ and any positive real numbers $r_1, r_2 > 0$, successive rescalings compose by multiplication of their factors. Specifically, 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$, denoted as $\text{scale}(r_1, \text{scale}(r_2, x)) = \text{scale}(r_1 \cdot r_2, x)$.

For any two units $x$ and $y$ of the same type $U$, if the ratio $y / x$ is a positive real number, then scaling the unit $x$ by the factor $y / x$ results in the unit $y$. In mathematical terms, this is expressed as $\text{scale}(y / x, x) = y$.