Physlib.Mathematics.RatComplexNum

For any two rational complex numbers $x$ and $y$, if their first components are equal ($x_1 = y_1$) and their second components are equal ($x_2 = y_2$), then the numbers themselves are equal ($x = y$).

The definition establishes an equivalence (a bijection) between the type of rational complex numbers, `RatComplexNum`, and the Cartesian product of rational numbers $\mathbb{Q} \times \mathbb{Q}$. A rational complex number $x$ is mapped to the pair of its components $(x_1, x_2)$, and conversely, a pair $(q_1, q_2) \in \mathbb{Q} \times \mathbb{Q}$ is mapped to the corresponding rational complex number.

Equality between any two rational complex numbers is decidable. This means that for any $x, y \in \text{RatComplexNum}$, there is a procedure to determine whether $x = y$. This decidability is derived from the fact that rational complex numbers are equivalent to pairs of rational numbers $\mathbb{Q} \times \mathbb{Q}$, and equality in $\mathbb{Q}$ is decidable.

The addition operation for rational complex numbers is defined component-wise. For any two rational complex numbers $x$ and $y$, represented as pairs of rational numbers $(x_{1}, x_{2})$ and $(y_{1}, y_{2})$, their sum is given by $x + y = (x_{1} + y_{1}, x_{2} + y_{2})$.

For any two rational complex numbers $x$ and $y$, the first component of their sum is equal to the sum of their individual first components, denoted as $(x + y)_{\text{fst}} = x_{\text{fst}} + y_{\text{fst}}$.

For any two rational complex numbers $x$ and $y$, the second component of their sum is equal to the sum of their individual second components, denoted as $(x + y)_{\text{snd}} = x_{\text{snd}} + y_{\text{snd}}$.

The type of rational complex numbers, represented as pairs of rational numbers $(x_1, x_2)$ corresponding to the real and imaginary parts, forms an additive abelian group ($\text{AddCommGroup}$). The zero element is defined as $(0, 0)$, addition is performed component-wise such that $(x_1, x_2) + (y_1, y_2) = (x_1 + y_1, x_2 + y_2)$, and the additive inverse is given by $-(x_1, x_2) = (-x_1, -x_2)$. Scalar multiplication by natural numbers $n \cdot x$ and integers $z \cdot x$ is also defined component-wise.

For two rational complex numbers $x = (x_1, x_2)$ and $y = (y_1, y_2)$, their product $x \cdot y$ is defined as the rational complex number $(x_1 y_1 - x_2 y_2, x_1 y_2 + x_2 y_1)$. Here, the first component represents the real part and the second component represents the imaginary part.

For any two rational complex numbers $x$ and $y$, the real part of their product is given by $(x \cdot y)_{\text{fst}} = x_{\text{fst}} y_{\text{fst}} - x_{\text{snd}} y_{\text{snd}}$, where $\text{fst}$ and $\text{snd}$ denote the real and imaginary components respectively.

For any two rational complex numbers $x$ and $y$, the imaginary part of their product is given by $(x \cdot y)_{\text{snd}} = x_{\text{fst}} y_{\text{snd}} + x_{\text{snd}} y_{\text{fst}}$, where $\text{fst}$ and $\text{snd}$ denote the real and imaginary components respectively.

The type of rational complex numbers $\text{RatComplexNum}$, consisting of pairs of rational numbers $(a, b) \in \mathbb{Q} \times \mathbb{Q}$ representing the real and imaginary parts, forms a ring. The addition is defined component-wise, and the multiplication of two elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ is given by $x \cdot y = (x_1 y_1 - x_2 y_2, x_1 y_2 + x_2 y_1)$. The multiplicative identity is defined as $1 = (1, 0)$.

For the multiplicative identity $1$ in the rational complex numbers $\text{RatComplexNum}$, its real component (the first part of the pair) is equal to $1$. That is, $(1)_{\text{fst}} = 1$.

In the ring of rational complex numbers $\text{RatComplexNum}$, where an element is represented as a pair of rational numbers $(a, b) \in \mathbb{Q} \times \mathbb{Q}$, the imaginary part (the second component) of the multiplicative identity $1$ is equal to $0$.

The first component (representing the real part) of the zero element $0$ in the ring of rational complex numbers $\text{RatComplexNum}$ is equal to $0$.

In the ring of rational complex numbers $\text{RatComplexNum}$, the second component (representing the imaginary part) of the zero element $0$ is equal to $0$.

The map $\text{toComplexNum} : \text{RatComplexNum} \to \mathbb{C}$ is a ring homomorphism that embeds a rational complex number $x = (a, b)$ into the field of complex numbers $\mathbb{C}$ as $a + bi$, where $a, b \in \mathbb{Q}$ are the real and imaginary parts of $x$ respectively, and $i$ is the imaginary unit.

Let $\text{RatComplexNum}$ be the ring of rational complex numbers, where an element $(x_1, x_2)$ represents the rational complex number $x_1 + x_2 i$. Let $\text{toComplexNum} : \text{RatComplexNum} \to \mathbb{C}$ be the ring homomorphism that embeds these numbers into the complex field $\mathbb{C}$. For any $a \in \text{RatComplexNum}$, the product of the imaginary unit $i \in \mathbb{C}$ and the embedding of $a$ is equal to the embedding of the product of the rational complex number $\langle 0, 1 \rangle$ and $a$. That is, $i \cdot \text{toComplexNum}(a) = \text{toComplexNum}(\langle 0, 1 \rangle \cdot a)$.

For any natural number $n \in \mathbb{N}$ and any rational complex number $a \in \text{RatComplexNum}$, it holds that $n \cdot \text{toComplexNum}(a) = \text{toComplexNum}(n \cdot a)$. Here, $\text{toComplexNum} : \text{RatComplexNum} \to \mathbb{C}$ is the ring homomorphism that embeds a rational complex number into the complex numbers $\mathbb{C}$ as $x + yi$.

The map $\text{toComplexNum} : \text{RatComplexNum} \to \mathbb{C}$, which embeds the rational complex numbers (numbers of the form $a + bi$ where $a, b \in \mathbb{Q}$) into the field of complex numbers $\mathbb{C}$, is injective.