Zsqrtd.coe_int_re
theorem Zsqrtd.coe_int_re : ∀ {d : ℤ} (n : ℤ), (↑n).re = n
This theorem states that for any integer `d` and any integer `n`, the real part (`re`) of the complex number obtained by casting `n` (i.e., `↑n`) is equal to `n` itself. In other words, when any integer is considered as a complex number, its real part is the integer itself.
More concisely: The real part of an integer `n` considered as a complex number equals `n` itself.
|
Zsqrtd.nonnegg_neg_pos
theorem Zsqrtd.nonnegg_neg_pos : ∀ {c d a b : ℕ}, Zsqrtd.Nonnegg c d (-↑a) ↑b ↔ Zsqrtd.SqLe a d b c
The theorem `Zsqrtd.nonnegg_neg_pos` states that for all natural numbers `c`, `d`, `a`, and `b`, the property `Zsqrtd.Nonnegg c d (-↑a) ↑b` holds if and only if `Zsqrtd.SqLe a d b c` is true. This means that a negative integer times the square root of `c` plus a positive integer times the square root of `d` is non-negative if and only if the square of the natural number `a` multiplied by `d` is less than or equal to the square of the natural number `b` multiplied by `c`. In mathematical terms, `-a √c + b √d ≥ 0` if and only if `d * a^2 ≤ c * b^2`.
More concisely: The theorem `Zsqrtd.nonnegg_neg_pos` asserts that `-a * sqrt(c) + b * sqrt(d) >= 0` is equivalent to `d * a^2 <= c * b^2`.
|
Zsqrtd.norm_mul
theorem Zsqrtd.norm_mul : ∀ {d : ℤ} (n m : ℤ√d), (n * m).norm = n.norm * m.norm
This theorem states that for any integer `d` and any two elements `n` and `m` of the set of integers adjoined with the square root of `d` (denoted as `ℤ√d`), the norm of the product of `n` and `m` is equal to the product of the norms of `n` and `m`. In other words, the norm function in the `ℤ√d` number field is multiplicative. This can be described mathematically as `∀ d ∈ ℤ, ∀ n, m ∈ ℤ√d, norm(n*m) = norm(n) * norm(m)`. Here, `norm(n)` refers to the norm of an element `n` in `ℤ√d`, which is defined as the difference between the square of `n`'s real part and `d` times the square of `n`'s imaginary part.
More concisely: For any integers $d, n, m$ in the number field $\mathbb{Z}[\sqrt{d}],$ the norm of their product $n \cdot m$ equals the product of their individual norms, i.e., $\|n \cdot m\| = \|n\| \cdot \|m\|.$
|
Zsqrtd.nonnegg_pos_neg
theorem Zsqrtd.nonnegg_pos_neg : ∀ {c d a b : ℕ}, Zsqrtd.Nonnegg c d (↑a) (-↑b) ↔ Zsqrtd.SqLe b c a d
The theorem `Zsqrtd.nonnegg_pos_neg` states that for any natural numbers `c`, `d`, `a`, and `b`, the condition `Zsqrtd.Nonnegg c d (↑a) (-↑b)` is equivalent to `Zsqrtd.SqLe b c a d`. In simpler terms, it says that `a √c - b √d ≥ 0` if and only if `b√c ≤ a√d`.
More concisely: The theorem `Zsqrtd.nonnegg_pos_neg` in Lean 4 asserts that for natural numbers `c`, `d`, `a`, and `b`, `a√c - b√d ≥ 0` if and only if `b√c ≤ a√d`.
|
Zsqrtd.ext_iff
theorem Zsqrtd.ext_iff : ∀ {d : ℤ} (x y : ℤ√d), x = y ↔ x.re = y.re ∧ x.im = y.im
This theorem states that for any integer `d` and for any two Zsqrtd objects `x` and `y`, `x` and `y` are equal if and only if the real part (`re`) and the imaginary part (`im`) of `x` are equal to the real and imaginary parts of `y`, respectively. In other words, two complex numbers with integer coefficients (also referred to as Gaussian integers) are equal if their corresponding real and imaginary components are equal.
More concisely: Two Zsqrtd objects `x` and `y` with integer coefficients are equal if and only if their real parts `re x` and `re y` are equal and their imaginary parts `im x` and `im y` are equal.
|
Zsqrtd.norm_eq_mul_conj
theorem Zsqrtd.norm_eq_mul_conj : ∀ {d : ℤ} (n : ℤ√d), ↑n.norm = n * star n
The theorem `Zsqrtd.norm_eq_mul_conj` states that for any integer `d` and any element `n` from the integer ring `ℤ[√d]`, the norm of `n` (as defined by the function `Zsqrtd.norm`) is equal to the product of `n` and its conjugate (where the conjugate is denoted by `star n`). In mathematical terms, this means that if `n` is an element of `ℤ[√d]`, then the norm of `n` (represented as `n.re * n.re - d * n.im * n.im`) is equal to the product of `n` and its conjugate.
More concisely: For any integer `d` and element `n` in the integer ring `ℤ[√d]`, the norm of `n` equals the product of `n` and its conjugate: `n.re * n.re - d * n.im * n.im = n * star n`.
|
Zsqrtd.ext
theorem Zsqrtd.ext : ∀ {d : ℤ} (x y : ℤ√d), x.re = y.re → x.im = y.im → x = y
This theorem states that for any integer `d` and any two numbers `x` and `y` in the space of integer square roots of `d` (notated as `ℤ√d`), if the real part of `x` is equal to the real part of `y` and the imaginary part of `x` is equal to the imaginary part of `y`, then `x` is equal to `y`. Essentially, it's expressing the concept that two complex numbers are equal if and only if both their real parts and their imaginary parts are equal.
More concisely: If two complex numbers with integer square root coefficients have equal real and imaginary parts, then they are equal.
|
Zsqrtd.norm_eq_one_iff_mem_unitary
theorem Zsqrtd.norm_eq_one_iff_mem_unitary : ∀ {d : ℤ} {a : ℤ√d}, a.norm = 1 ↔ a ∈ unitary (ℤ√d)
This theorem states that for any integer `d` and any element `a` of the integer quadratic field `ℤ√d`, `a` has a norm equal to `1` if and only if it is contained in the submonoid of unitary elements of `ℤ√d`. In other words, an element of `ℤ√d` has a norm of `1` precisely when it belongs to the set of elements `U` in `ℤ√d` such that the product of `U` and its conjugate (given by the `star` operation) is `1`, both when `U` is multiplied by its conjugate before and after.
More concisely: An element of the integer quadratic field `ℤ√d` has norm equal to 1 if and only if it belongs to the submonoid of unitary elements, i.e., elements whose product with their conjugate is 1.
|
Zsqrtd.smul_val
theorem Zsqrtd.smul_val : ∀ {d : ℤ} (n x y : ℤ), ↑n * { re := x, im := y } = { re := n * x, im := n * y }
This theorem establishes the scalar multiplication operation in Z[sqrt(d)], the ring of integers extended by the square root of an integer d. For any integer d, and any integers n, x, and y, the product of n and the complex number with real part x and imaginary part y is equal to the complex number with real part n*x and imaginary part n*y. In other words, multiplication distributes over the real and imaginary components of the complex number.
More concisely: For any integer d in Z, and any integers n, x, and y, the operation (n : Z[sqrt d]) * (x + i*y) = n*x + i*n*y holds in the ring Z[sqrt d], where i is the imaginary unit.
|
Zsqrtd.norm_zero
theorem Zsqrtd.norm_zero : ∀ {d : ℤ}, Zsqrtd.norm 0 = 0
The theorem `Zsqrtd.norm_zero` states that for all integers `d`, the norm of the complex number `0` in the integer ring `ℤ[√d]` is `0`. This norm is calculated as the real part of the number squared minus `d` times the imaginary part of the number squared. In other words, for any integer `d`, the norm function `Zsqrtd.norm` when applied to the complex number `0`, always yields `0`.
More concisely: The norm of the complex number 0 in the ring of integers ℤ[√d] is 0.
|
Zsqrtd.mker_norm_eq_unitary
theorem Zsqrtd.mker_norm_eq_unitary : ∀ {d : ℤ}, MonoidHom.mker Zsqrtd.normMonoidHom = unitary (ℤ√d)
This theorem states that for any integer `d`, the multiplicative kernel of the norm map on the ring of integers adjoined with the square root of `d` (denoted as `ℤ√d`) is equal to the submonoid of unitary elements in `ℤ√d`. The multiplicative kernel of the norm map consists of elements `x` in `ℤ√d` such that the norm of `x` equals 1. On the other hand, the unitary elements in `ℤ√d` are those that satisfy the condition that the product of an element and its conjugate (the star of the element) equals 1, both when the element is on the left and on the right of the multiplication. The theorem thus provides a connection between the norm function and the concept of unitary elements in this context.
More concisely: The multiplicative kernel of the norm map on the ring of integers adjoined with the square root of `d` equals the submonoid of unitary elements.
|
Zsqrtd.lift_injective
theorem Zsqrtd.lift_injective :
∀ {R : Type} [inst : CommRing R] [inst_1 : CharZero R] {d : ℤ} (r : { r // r * r = ↑d }),
(∀ (n : ℤ), d ≠ n * n) → Function.Injective ⇑(Zsqrtd.lift r)
The theorem `Zsqrtd.lift_injective` states that for any type `R` endowed with a commutative ring structure and characteristic zero and for any integer `d`, given a root `r` such that `r` times `r` equals `d`, if `d` is not a perfect square (i.e., there does not exist an integer `n` such that `d` equals `n` times `n`), then the unique ring homomorphism from the ring of integers adjoined by the square root of `d` to `R`, constructed by replacing the square root of `d` with `r`, is injective (i.e., if the homomorphism maps two elements to the same element in `R`, then those two elements were the same in the first place). This injective property relies on the fact that the map from the integers into `R` is also injective (characteristic zero).
More concisely: If `R` is a commutative ring with characteristic zero, and `d` is an non-square integer such that `r^2 = d` in `R`, then the ring homomorphism from the integers adjoined by the square root of `d` to `R`, sending the square root of `d` to `r`, is injective.
|
Zsqrtd.coe_int_im
theorem Zsqrtd.coe_int_im : ∀ {d : ℤ} (n : ℤ), (↑n).im = 0
This theorem states that for any integer `n` and any integer `d`, the imaginary part of `n` when it is cast to a complex number (`↑n`) is equal to `0`. This result is expected because integers are real numbers, and real numbers have no imaginary part: their imaginary part is always `0`.
More concisely: For any integer `n`, the imaginary part of the complex number `↑n` is equal to 0.
|
Zsqrtd.nonneg_cases
theorem Zsqrtd.nonneg_cases :
∀ {d : ℕ} {a : ℤ√↑d},
a.Nonneg → ∃ x y, a = { re := ↑x, im := ↑y } ∨ a = { re := ↑x, im := -↑y } ∨ a = { re := -↑x, im := ↑y }
The theorem `Zsqrtd.nonneg_cases` states that for any natural number `d` and an element `a` of the quadratic integer ring `ℤ√↑d` which is nonnegative (as defined by `Zsqrtd.Nonneg`), there exist integers `x` and `y` such that `a` is equal to `x + yi`, `x - yi`, or `-x + yi`. That is, any nonnegative element of the quadratic integer ring can be expressed in one of these three forms.
More concisely: For any nonnegative element `a` in the quadratic integer ring `ℤ√↑d`, there exist integers `x` and `y` such that `a` can be expressed as `x + yi`, `x - yi`, or `-x + yi`.
|
Zsqrtd.norm_eq_one_iff
theorem Zsqrtd.norm_eq_one_iff : ∀ {d : ℤ} {x : ℤ√d}, x.norm.natAbs = 1 ↔ IsUnit x
This theorem states that for any integer `d` and any element `x` from the ring of integers adjoined with the square root of `d`, the absolute value of the norm of `x` being 1 is equivalent to `x` being a unit in that ring. In other words, an element `x` in `ℤ[√d]` is a unit if and only if the absolute value of its norm is 1. Here, a unit is an element with a multiplicative inverse.
More concisely: In the ring of integers adjoined with the square root of a given integer `d`, an element `x` is a unit if and only if the absolute value of its norm is 1.
|