Physlib.Electromagnetism.Charge.ChargeUnit

For any electric charge unit $x$, its underlying numerical real value $x.\text{val}$ is not equal to zero.

For any unit of electric charge $x \in \text{ChargeUnit}$, its underlying numerical real value $x.\text{val}$ is strictly positive, i.e., $x.\text{val} > 0$.

The type `ChargeUnit` represents the set of possible units for electric charge, which are modeled as positive real numbers $\mathbb{R}^+$. The statement establishes that `ChargeUnit` is inhabited, meaning it possesses a default element. This default element is defined to have the underlying numerical value $1$, which, according to the provided context, corresponds to the unit of the coulomb.

For any two units of charge $x, y \in \text{ChargeUnit}$, the quotient $x / y$ is defined as the ratio of their underlying positive real values $\frac{\text{val}(x)}{\text{val}(y)}$, resulting in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any two charge units $x, y \in \text{ChargeUnit}$, the quotient $x / y$ is equal to the ratio of their underlying numerical values $\frac{x.\text{val}}{y.\text{val}}$, considered as a non-negative real number in $\mathbb{R}_{\ge 0}$. Here, $x.\text{val}$ and $y.\text{val}$ represent the positive real numbers associated with the units $x$ and $y$ respectively.

For any two units of charge $x, y \in \text{ChargeUnit}$, their quotient $x / y$ is not equal to zero in the non-negative real numbers $\mathbb{R}_{\ge 0}$. Here, the quotient $x / y$ represents the ratio of the underlying positive real values associated with each charge unit.

For any two units of charge $x, y \in \text{ChargeUnit}$, their quotient $x / y$ is strictly greater than zero in the non-negative real numbers $\mathbb{R}_{\ge 0}$. Here, the quotient $x / y$ represents the ratio of the underlying positive real values associated with each charge unit.

For any unit of charge $x \in \text{ChargeUnit}$, the ratio $x / x$ is equal to $1 \in \mathbb{R}_{\ge 0}$.

For any two units of charge $x, y \in \text{ChargeUnit}$, the ratio $x/y$ is equal to the multiplicative inverse of the ratio $y/x$, which is expressed as $x / y = (y / x)^{-1}$ in the non-negative real numbers $\mathbb{R}_{\ge 0}$.

For any three units of charge $x, y, z \in \text{ChargeUnit}$, the product of the ratio $x/y$ and the ratio $y/z$ is equal to the ratio $x/z$, where these ratios are treated as real numbers.

For any unit of charge $x \in \text{ChargeUnit}$ and any positive real number $r \in \mathbb{R}$ ($r > 0$), scaling the unit $x$ by the factor $r$ (denoted as $\text{scale}(r, x, hr)$) and then dividing by the original unit $x$ yields the ratio $r$ as a non-negative real number: $$\frac{\text{scale}(r, x, hr)}{x} = r$$

Let $x$ be a unit of charge ($x \in \text{ChargeUnit}$). For any positive real number $r > 0$, let $\text{scale}(r, x)$ denote the charge unit $x$ scaled by the factor $r$. The ratio of the original unit $x$ to its scaled version is given by: $$\frac{x}{\text{scale}(r, x)} = \frac{1}{r}$$ where the division represents the ratio of their underlying values as a non-negative real number in $\mathbb{R}_{\ge 0}$.

Let $x$ be a unit of charge ($\text{ChargeUnit}$). Scaling the charge unit $x$ by a factor of $1$ results in the original charge unit: $$\text{scale}(1, x) = x$$

Let $x_1$ and $x_2$ be units of charge ($\text{ChargeUnit}$). For any positive real numbers $r_1, r_2 > 0$, let $\text{scale}(r, x)$ denote the scaling of a charge unit $x$ by a factor $r$. The ratio of the two scaled units satisfies: $$\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 the division of two charge units $u/v$ represents the ratio of their underlying values as a non-negative real number in $\mathbb{R}_{\ge 0}$.

Let $x$ be a unit of charge ($\text{ChargeUnit}$). For any positive real numbers $r_1, r_2 \in \mathbb{R}_{>0}$, let $\text{scale}(r, x)$ denote the scaling of a charge unit $x$ by a factor $r$. Successively scaling a charge unit by a factor $r_2$ and then by a factor $r_1$ is equivalent to scaling the original unit 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 coulomb is defined as the specific element of the type `ChargeUnit` that corresponds to the numerical value $1$. In this context, the type `ChargeUnit` is modeled as the set of positive real numbers $\mathbb{R}_{>0}$.

The elementary charge is defined as the unit of charge obtained by scaling the `coulombs` unit by the factor $1.602176634 \times 10^{-19}$. Within the model where the type `ChargeUnit` is identified with the set of positive real numbers $\mathbb{R}_{>0}$ and the `coulombs` unit corresponds to the value $1$, the elementary charge represents the value $1.602176634 \times 10^{-19}$.