The ring ℤ[√−2]

TheoremThe norm on \(\mathbb{Z}(\sqrt{-2})\) is nonnegative#✓fully proved

For every \(x = a + b\sqrt{-2}\) in \(\mathbb{Z}[\sqrt{-2}]\), the norm \(N(x) = a^2 + 2b^2\) satisfies \(N(x) \ge 0\).

public theorem norm_nonneg' (x : Zsqrtd (-2 : ℤ)) : 0 ≤ x.norm

Used by 3

Used byThe norm on \(\mathbb{Z}(\sqrt{-2})\) equals its absolute value · The remainder is smaller than the divisor, in absolute norm · Nonzero elements of \(\mathbb{Z}(\sqrt{-2})\) have positive norm

TheoremThe norm on \(\mathbb{Z}(\sqrt{-2})\) vanishes only at zero#✓fully proved

For \(x = a + b\sqrt{-2}\) in \(\mathbb{Z}[\sqrt{-2}]\) with norm \(N(x) = a^2 + 2b^2\), we have \(N(x) = 0\) if and only if \(x = 0\).

public theorem norm_eq_zero' {x : Zsqrtd (-2 : ℤ)} : x.norm = 0 ↔ x = 0

Used by 1

Used byNonzero elements of \(\mathbb{Z}(\sqrt{-2})\) have positive norm

TheoremNonzero elements of \(\mathbb{Z}(\sqrt{-2})\) have positive norm#✓fully proved

For \(x = a + b\sqrt{-2}\) in \(\mathbb{Z}[\sqrt{-2}]\) with norm \(N(x) = a^2 + 2b^2\), we have \(N(x) > 0\) if and only if \(x \ne 0\).

public theorem norm_pos' {x : Zsqrtd (-2 : ℤ)} : 0 < x.norm ↔ x ≠ 0

Uses 2 · Used by 2

Proof usesThe norm on \(\mathbb{Z}(\sqrt{-2})\) vanishes only at zero · The norm on \(\mathbb{Z}(\sqrt{-2})\) is nonnegative

Used byMultiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\)

TheoremThe norm on \(\mathbb{Z}(\sqrt{-2})\) equals its absolute value#✓fully proved

For every \(x = a + b\sqrt{-2}\) in \(\mathbb{Z}[\sqrt{-2}]\), the norm \(N(x) = a^2 + 2b^2\) satisfies \(|N(x)| = N(x)\), where \(|N(x)|\) is taken as a natural number and read back as an integer.

public theorem abs_natCast_norm' (x : Zsqrtd (-2 : ℤ)) :
    (x.norm.natAbs : ℤ) = x.norm

Uses 1 · Used by 1

Proof usesThe norm on \(\mathbb{Z}(\sqrt{-2})\) is nonnegative

Used byMultiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\)

TheoremRounding division on \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Let \(x, y \in \mathbb{Z}[\sqrt{-2}]\) with \(y = c + d\sqrt{-2}\), let \(\bar{y} = c - d\sqrt{-2}\) be its conjugate and \(N(y) = c^2 + 2d^2\) its norm, and write \(x\bar{y} = u + v\sqrt{-2}\) with \(u, v \in \mathbb{Z}\). The quotient is \(x / y = \operatorname{round}(u / N(y)) + \operatorname{round}(v / N(y))\sqrt{-2}\), where \(u / N(y)\) and \(v / N(y)\) are computed in \(\mathbb{Q}\) (division by \(0\) gives \(0\)) and \(\operatorname{round}\) sends a rational number to the nearest integer, rounding halves up.

public theorem div_def' (x y : Zsqrtd (-2 : ℤ)) :
    x / y = ⟨round ((x * star y).re / y.norm : ℚ),
      round ((x * star y).im / y.norm : ℚ)⟩

Used by 9

Used byThe remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\) · Primes congruent to 5 or 7 mod 8 are inert in ℤ(√−2) · Elements of ℤ(√−2) of prime norm are prime · Primes \(p \equiv 1, 3 \pmod 8\) are norms of primes of \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremRemainder of the rounding division on \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

For all \(x, y\) in \(\mathbb{Z}[\sqrt{-2}]\), the remainder is \(x \bmod y = x - y\,(x / y)\), where \(x / y\) is the rounding division of \(\mathbb{Z}[\sqrt{-2}]\).

public theorem mod_def' (x y : Zsqrtd (-2 : ℤ)) : x % y = x - y * (x / y)

Used by 1

Used byThe remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\)

TheoremError of rounded integer division#✓fully proved

Let \(a\) and \(N\) be integers with \(N > 0\), and let \(q\) be the integer nearest to the rational number \(a/N\) (halves rounded up). Then \(|2(a - qN)| \le N\), that is, \(a\) differs from \(qN\) by at most \(N/2\).

public theorem round_error (a N : ℤ) (hN : 0 < N) :
    |2 * (a - round (a / N : ℚ) * N)| ≤ N

Used by 1

Used byThe remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\)

TheoremNorm identity for the remainder#✓fully proved

Let \(x, y, q \in \mathbb{Z}[\sqrt{-2}]\), write \(N(a + b\sqrt{-2}) = a^2 + 2b^2\) for the norm and \(\bar{y}\) for the conjugate of \(y\), and write \(x\bar{y} = u + v\sqrt{-2}\) and \(q = e + f\sqrt{-2}\) with \(u, v, e, f \in \mathbb{Z}\). Then \(N(y)\,N(x - yq) = (u - N(y)\,e)^2 + 2\,(v - N(y)\,f)^2\).

public theorem norm_key (x y q : Zsqrtd (-2 : ℤ)) :
    y.norm * (x - y * q).norm
      = ((x * star y).re - y.norm * q.re) * ((x * star y).re - y.norm * q.re)
        + 2 * (((x * star y).im - y.norm * q.im)
          * ((x * star y).im - y.norm * q.im))

Used by 1

Used byThe remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\)

TheoremThe remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Let \(x, y\) be elements of \(\mathbb{Z}[\sqrt{-2}]\) with \(y \ne 0\), and let \(N(a + b\sqrt{-2}) = a^2 + 2b^2\) be the norm. The remainder \(x \bmod y = x - y\,(x / y)\) of the rounding division of \(\mathbb{Z}[\sqrt{-2}]\) satisfies \(N(x \bmod y) < N(y)\).

public theorem norm_mod_lt' (x : Zsqrtd (-2 : ℤ)) {y : Zsqrtd (-2 : ℤ)}
    (hy : y ≠ 0) : (x % y).norm < y.norm

Uses 5 · Used by 1

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · Remainder of the rounding division on \(\mathbb{Z}(\sqrt{-2})\) · Norm identity for the remainder · Nonzero elements of \(\mathbb{Z}(\sqrt{-2})\) have positive norm · Error of rounded integer division

Used byThe remainder is smaller than the divisor, in absolute norm

TheoremThe remainder is smaller than the divisor, in absolute norm#✓fully proved

Let \(x, y\) be elements of \(\mathbb{Z}[\sqrt{-2}]\) with \(y \ne 0\), and let \(N(a + b\sqrt{-2}) = a^2 + 2b^2\) be the norm. The remainder \(x \bmod y = x - y\,(x / y)\) of the rounding division of \(\mathbb{Z}[\sqrt{-2}]\) satisfies \(|N(x \bmod y)| < |N(y)|\) as natural numbers.

public theorem natAbs_norm_mod_lt' (x : Zsqrtd (-2 : ℤ)) {y : Zsqrtd (-2 : ℤ)}
    (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs

Uses 2 · Used by 8

Proof usesThe remainder is smaller than the divisor in \(\mathbb{Z}(\sqrt{-2})\) · The norm on \(\mathbb{Z}(\sqrt{-2})\) is nonnegative

Used byPrimes congruent to 5 or 7 mod 8 are inert in ℤ(√−2) · Elements of ℤ(√−2) of prime norm are prime · Primes \(p \equiv 1, 3 \pmod 8\) are norms of primes of \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremMultiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Let \(N(a + b\sqrt{-2}) = a^2 + 2b^2\) be the norm on \(\mathbb{Z}[\sqrt{-2}]\). For \(x, y \in \mathbb{Z}[\sqrt{-2}]\) with \(y \ne 0\), we have \(|N(x)| \le |N(xy)|\) as natural numbers.

public theorem norm_le_norm_mul_left' (x : Zsqrtd (-2 : ℤ)) {y : Zsqrtd (-2 : ℤ)}
    (hy : y ≠ 0) : x.norm.natAbs ≤ (x * y).norm.natAbs

Uses 2 · Used by 8

Proof usesThe norm on \(\mathbb{Z}(\sqrt{-2})\) equals its absolute value · Nonzero elements of \(\mathbb{Z}(\sqrt{-2})\) have positive norm

Used byPrimes congruent to 5 or 7 mod 8 are inert in ℤ(√−2) · Elements of ℤ(√−2) of prime norm are prime · Primes \(p \equiv 1, 3 \pmod 8\) are norms of primes of \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremUnits of ℤ(√−2)#✓fully proved

An element \(x\) of \(\mathbb{Z}[\sqrt{-2}]\) is a unit if and only if \(x = 1\) or \(x = -1\).

public theorem zsqrtd_neg_two_isUnit_iff (x : ℤ√(-2 : ℤ)) :
    IsUnit x ↔ x = 1 ∨ x = -1

Used by 3

Used byEvery unit of ℤ(√−2) is enumerated · Conjugate factorization of an odd prime in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\)

TheoremElements of ℤ(√−2) of prime norm are prime#✓fully proved

For \(\pi = a + b\sqrt{-2}\) in \(\mathbb{Z}[\sqrt{-2}]\) let \(N(\pi) = a^2 + 2b^2\) be its norm. If \(|N(\pi)|\) is a prime number, then \(\pi\) is a prime element of \(\mathbb{Z}[\sqrt{-2}]\).

public theorem zsqrtd_neg_two_prime_of_natAbs_norm_prime {π : ℤ√(-2 : ℤ)}
    (h : (Zsqrtd.norm π).natAbs.Prime) : Prime π

Uses 4 · Used by 3

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{d})\) of prime norm are prime

Used by√−2 is prime in ℤ(√−2) · Primes \(p \equiv 1, 3 \pmod 8\) are norms of primes of \(\mathbb{Z}(\sqrt{-2})\) · Conjugate factorization of an odd prime in \(\mathbb{Z}(\sqrt{-2})\)

Theorem√−2 is prime in ℤ(√−2)#✓fully proved

The element \(\sqrt{-2}\) is a prime element of \(\mathbb{Z}[\sqrt{-2}]\).

Its norm is \(2\), a prime number.

public theorem zsqrtd_neg_two_prime_sqrtd : Prime (⟨0, 1⟩ : ℤ√(-2 : ℤ))

Uses 1 · Used by 1

Proof usesElements of ℤ(√−2) of prime norm are prime

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\)

Theorem\(2\) is minus the square of \(\sqrt{-2}\)#✓fully proved

In \(\mathbb{Z}[\sqrt{-2}]\) one has \(2 = -(\sqrt{-2})^2\).

public theorem zsqrtd_neg_two_two_eq : (2 : ℤ√(-2 : ℤ)) = -⟨0, 1⟩ ^ 2

Theoremx² + 2y² is never 5 or 7 modulo 8#✓fully proved

For all \(x, y \in \mathbb{Z}/8\mathbb{Z}\), \(x^2 + 2y^2 \ne 5\) and \(x^2 + 2y^2 \ne 7\).

public theorem zsqrtd_neg_two_mod8_obstruction :
    ∀ x y : ZMod 8, x ^ 2 + 2 * y ^ 2 ≠ 5 ∧ x ^ 2 + 2 * y ^ 2 ≠ 7

Used by 1

Used byPrimes congruent to 5 or 7 mod 8 are inert in ℤ(√−2)

TheoremPrimes congruent to 5 or 7 mod 8 are inert in ℤ(√−2)#✓fully proved

If \(p\) is a prime number with \(p \equiv 5 \pmod 8\) or \(p \equiv 7 \pmod 8\), then \(p\) is a prime element of \(\mathbb{Z}[\sqrt{-2}]\).

public theorem zsqrtd_neg_two_inert {p : ℕ} [Fact p.Prime]
    (h : p % 8 = 5 ∨ p % 8 = 7) : Prime (p : ℤ√(-2 : ℤ))

Uses 4 · Used by 1

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · x² + 2y² is never 5 or 7 modulo 8

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime

TheoremPrimes \(p \equiv 1, 3 \pmod 8\) are norms of primes of \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Let \(p\) be a prime number with \(p \equiv 1 \pmod 8\) or \(p \equiv 3 \pmod 8\). Then there is a prime element \(\pi = a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\) whose norm \(a^2 + 2b^2\) equals \(p\).

public theorem zsqrtd_neg_two_split {p : ℕ} [Fact p.Prime]
    (h : p % 8 = 1 ∨ p % 8 = 3) :
    ∃ π : ℤ√(-2 : ℤ), Zsqrtd.norm π = p ∧ Prime π

Uses 4 · Used by 1

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Elements of ℤ(√−2) of prime norm are prime

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremConjugate factorization of an odd prime in \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Let \(p\) be an odd prime number and let \(\pi = a + b\sqrt{-2}\) be an element of \(\mathbb{Z}[\sqrt{-2}]\) whose norm \(a^2 + 2b^2\) equals \(p\). Write \(\bar\pi = a - b\sqrt{-2}\) for the conjugate of \(\pi\). Then \(p = \pi\bar\pi\), \(\bar\pi\) is prime in \(\mathbb{Z}[\sqrt{-2}]\), and \(\bar\pi\) is not associated to \(\pi\).

public theorem zsqrtd_neg_two_split_conj {p : ℕ} [Fact p.Prime] {π : ℤ√(-2 : ℤ)}
    (hnorm : Zsqrtd.norm π = p) (hodd : p % 2 = 1) :
    (p : ℤ√(-2 : ℤ)) = π * star π ∧ Prime (star π) ∧ ¬ Associated (star π) π

Uses 2 · Used by 1

Proof usesUnits of ℤ(√−2) · Elements of ℤ(√−2) of prime norm are prime

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime

DefinitionEnumeration of the units of ℤ(√−2)#✓fully proved

The map \(\{0, 1\} \to \mathbb{Z}[\sqrt{-2}]\) sending \(0\) to \(1\) and \(1\) to \(-1\), which lists the two units of \(\mathbb{Z}[\sqrt{-2}]\).

public def unitVal : Fin 2 → ℤ√(-2 : ℤ) :=
  fun i => if i = 0 then 1 else -1

Used by 8

Used byEvery unit of ℤ(√−2) is enumerated · The enumeration of the units of ℤ(√−2) is injective · Each enumerated unit of ℤ(√−2) times its listed inverse is one · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremThe enumeration of the units of ℤ(√−2) is injective#✓fully proved

Let \(\varepsilon_0 = 1\) and \(\varepsilon_1 = -1\) in \(\mathbb{Z}[\sqrt{-2}]\). For \(i, j \in \{0, 1\}\), if \(\varepsilon_i = \varepsilon_j\) then \(i = j\).

public theorem unitVal_inj : Function.Injective unitVal

Uses 1 · Used by 5

Statement usesEnumeration of the units of ℤ(√−2)

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremEvery unit of ℤ(√−2) is enumerated#✓fully proved

Let \(\varepsilon_0 = 1\) and \(\varepsilon_1 = -1\) be the enumeration of the units of \(\mathbb{Z}[\sqrt{-2}]\). Every unit \(u\) of \(\mathbb{Z}[\sqrt{-2}]\) equals \(\varepsilon_i\) for some \(i \in \{0, 1\}\).

public theorem unitVal_complete (u : ℤ√(-2 : ℤ)) (hu : IsUnit u) :
    ∃ i, unitVal i = u

Uses 2 · Used by 5

Statement usesEnumeration of the units of ℤ(√−2)

Proof usesUnits of ℤ(√−2)

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

DefinitionInverses of the enumerated units of ℤ(√−2)#✓fully proved

The map \(\{0, 1\} \to \mathbb{Z}[\sqrt{-2}]\) sending \(0\) to \(1\) and \(1\) to \(-1\). Since \(1\) and \(-1\) are their own inverses, its value at \(i\) is the inverse of the \(i\)-th enumerated unit.

public def unitValInv : Fin 2 → ℤ√(-2 : ℤ) :=
  fun i => if i = 0 then 1 else -1

Used by 6

Used byEach enumerated unit of ℤ(√−2) times its listed inverse is one · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremEach enumerated unit of ℤ(√−2) times its listed inverse is one#✓fully proved

Let \(\varepsilon_0 = 1\), \(\varepsilon_1 = -1\) be the enumerated units of \(\mathbb{Z}[\sqrt{-2}]\) and \(\eta_0 = 1\), \(\eta_1 = -1\) their listed inverses. Then \(\varepsilon_i \eta_i = 1\) for each \(i \in \{0, 1\}\).

public theorem unitVal_mul_unitValInv (i : Fin 2) :
    unitVal i * unitValInv i = 1

Uses 2 · Used by 5

Statement usesEnumeration of the units of ℤ(√−2) · Inverses of the enumerated units of ℤ(√−2)

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.