Gaussian primes

TheoremUnits of the Gaussian integers#✓fully proved

A Gaussian integer \(x \in \mathbb{Z}[i]\) is a unit if and only if \(x\) is one of \(1\), \(-1\), \(i\) and \(-i\).

public theorem gaussianInt_isUnit_iff (x : ℤ[i]) :
    IsUnit x ↔ x = 1 ∨ x = -1 ∨ x = ⟨0, 1⟩ ∨ x = ⟨0, -1⟩

Used by 2

Used byGaussian integers of split prime norm are not associate to their conjugates · The enumeration of the Gaussian units is complete

TheoremGaussian integers of prime norm are prime#✓fully proved

Let \(\pi = a + bi \in \mathbb{Z}[i]\) and let \(N(\pi) = a^2 + b^2\) be its norm. If the absolute value of \(N(\pi)\) is a prime number, then \(\pi\) is a prime element of \(\mathbb{Z}[i]\).

public theorem gaussianInt_prime_of_natAbs_norm_prime {π : ℤ[i]}
    (h : (Zsqrtd.norm π).natAbs.Prime) : Prime π

Uses 1 · Used by 5

Proof usesElements of \(\mathbb{Z}(\sqrt{d})\) of prime norm are prime

Used byClassification of the Gaussian primes · 1 + i is a Gaussian prime · Factoring a prime as a Gaussian integer times its conjugate · Primes congruent to 1 mod 4 split in the Gaussian integers · Explicit Gaussian prime factors of a prime congruent to 1 mod 4

Theorem1 + i is a Gaussian prime#✓fully proved

The Gaussian integer \(1 + i\) is a prime element of \(\mathbb{Z}[i]\); its norm is \(2\).

public theorem gaussianInt_prime_one_add_I : Prime (⟨1, 1⟩ : ℤ[i])

Uses 1 · Used by 1

Proof usesGaussian integers of prime norm are prime

Used byJacobi's two-square theorem

TheoremFactorization of 2 in the Gaussian integers#✓fully proved

In \(\mathbb{Z}[i]\) we have \(2 = -i \cdot (1 + i)^2\), where \(-i\) is a unit with inverse \(i\).

public theorem gaussianInt_two_eq : (2 : ℤ[i])
    = (⟨⟨0, -1⟩, ⟨0, 1⟩, by decide, by decide⟩ : ℤ[i]ˣ) * ⟨1, 1⟩ ^ 2

Used by 1

Used byJacobi's two-square theorem

DefinitionEnumeration of the Gaussian units#✓fully proved

The map \(u\) on \(\{0, 1, 2, 3\}\) with \(u_0 = 1\), \(u_1 = -1\), \(u_2 = i\) and \(u_3 = -i\) in \(\mathbb{Z}[i]\), listing the four units of \(\mathbb{Z}[i]\).

public def unitVal : Fin 4 → ℤ[i] := fun i =>
  if i = 0 then 1 else if i = 1 then -1 else if i = 2 then ⟨0, 1⟩
    else ⟨0, -1⟩

Used by 5

Used byNumber of Gaussian integers of norm a power of a split prime · The enumeration of the Gaussian units is complete · The four Gaussian units are distinct · Each Gaussian unit times its listed inverse is one · Jacobi's two-square theorem

TheoremThe four Gaussian units are distinct#✓fully proved

Let \(u_0 = 1\), \(u_1 = -1\), \(u_2 = i\) and \(u_3 = -i\) in \(\mathbb{Z}[i]\). For \(j, k \in \{0, 1, 2, 3\}\), if \(u_j = u_k\) then \(j = k\).

public theorem unitVal_inj : Function.Injective unitVal

Uses 1 · Used by 2

Statement usesEnumeration of the Gaussian units

Used byNumber of Gaussian integers of norm a power of a split prime · Jacobi's two-square theorem

TheoremThe enumeration of the Gaussian units is complete#✓fully proved

Let \(u_0 = 1\), \(u_1 = -1\), \(u_2 = i\) and \(u_3 = -i\). Every unit \(u\) of \(\mathbb{Z}[i]\) equals \(u_j\) for some \(j \in \{0, 1, 2, 3\}\).

public theorem unitVal_complete (u : ℤ[i]) (hu : IsUnit u) :
    ∃ i, unitVal i = u

Uses 2 · Used by 2

Statement usesEnumeration of the Gaussian units

Proof usesUnits of the Gaussian integers

Used byNumber of Gaussian integers of norm a power of a split prime · Jacobi's two-square theorem

DefinitionInverses of the Gaussian units#✓fully proved

The map \(v\) on \(\{0, 1, 2, 3\}\) with \(v_0 = 1\), \(v_1 = -1\), \(v_2 = -i\) and \(v_3 = i\) in \(\mathbb{Z}[i]\), listing the inverses of the units \(1\), \(-1\), \(i\) and \(-i\) in that order.

public def unitValInv : Fin 4 → ℤ[i] := fun i =>
  if i = 0 then 1 else if i = 1 then -1 else if i = 2 then ⟨0, -1⟩
    else ⟨0, 1⟩

Used by 3

Used byNumber of Gaussian integers of norm a power of a split prime · Each Gaussian unit times its listed inverse is one · Jacobi's two-square theorem

TheoremEach Gaussian unit times its listed inverse is one#✓fully proved

Let \(u_0 = 1\), \(u_1 = -1\), \(u_2 = i\), \(u_3 = -i\) and \(v_0 = 1\), \(v_1 = -1\), \(v_2 = -i\), \(v_3 = i\) in \(\mathbb{Z}[i]\). Then \(u_j v_j = 1\) for every \(j \in \{0, 1, 2, 3\}\).

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

Uses 2 · Used by 2

Statement usesEnumeration of the Gaussian units · Inverses of the Gaussian units

Used byNumber of Gaussian integers of norm a power of a split prime · Jacobi's two-square theorem

TheoremExplicit Gaussian prime factors of a prime congruent to 1 mod 4#✓fully proved

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\). Then there are natural numbers \(a\) and \(b\) with \(a^2 + b^2 = p\) such that both \(a + bi\) and \(a - bi\) are prime elements of the Gaussian integers \(\mathbb{Z}[i]\).

public theorem gaussianInt_split_prime_sq_add_sq {p : ℕ} [Fact p.Prime]
    (h : p % 4 = 1) :
    ∃ a b : ℕ, a ^ 2 + b ^ 2 = p ∧ Prime (⟨(a : ℤ), (b : ℤ)⟩ : GaussianInt) ∧
      Prime (⟨(a : ℤ), -(b : ℤ)⟩ : GaussianInt)

Uses 1

Proof usesGaussian integers of prime norm are prime

TheoremClassification of the Gaussian primes#✓fully proved

Every prime element \(z\) of the Gaussian integers \(\mathbb{Z}[i]\) is associated to one of the following: a rational prime \(p\) with \(p \equiv 3 \pmod 4\); one of \(a + bi\) and \(a - bi\), where \(a\) and \(b\) are natural numbers with \(a^2 + b^2 = p\) for some rational prime \(p \equiv 1 \pmod 4\); or \(1 + i\).

public theorem gaussianInt_prime_associated (z : GaussianInt) (hz : Prime z) :
    (∃ p : ℕ, p.Prime ∧ p % 4 = 3 ∧ Associated z (p : GaussianInt)) ∨
      (∃ a b p : ℕ, p.Prime ∧ p % 4 = 1 ∧ a ^ 2 + b ^ 2 = p ∧
        (Associated z (⟨(a : ℤ), (b : ℤ)⟩ : GaussianInt) ∨
          Associated z (⟨(a : ℤ), -(b : ℤ)⟩ : GaussianInt))) ∨
      Associated z (⟨1, 1⟩ : GaussianInt)

Uses 1

Proof usesGaussian integers of prime norm are prime

TheoremPrimes congruent to 1 mod 4 split in the Gaussian integers#✓fully proved

Let \(p\) be a prime with \(p \equiv 1 \pmod 4\). Then there is a prime element \(\pi = a + bi\) of \(\mathbb{Z}[i]\) whose norm \(N(\pi) = a^2 + b^2\) equals \(p\).

public theorem gaussianInt_split_prime {p : ℕ} [Fact p.Prime] (h : p % 4 = 1) :
    ∃ π : ℤ[i], Zsqrtd.norm π = p ∧ Prime π

Uses 1 · Used by 1

Proof usesGaussian integers of prime norm are prime

Used byJacobi's two-square theorem

TheoremFactoring a prime as a Gaussian integer times its conjugate#✓fully proved

Let \(p\) be a prime, write \(N(a + bi) = a^2 + b^2\) for the norm on \(\mathbb{Z}[i]\), and let \(\pi \in \mathbb{Z}[i]\) satisfy \(N(\pi) = p\). Then \(p = \pi \bar{\pi}\) in \(\mathbb{Z}[i]\), where \(\bar{\pi}\) is the complex conjugate of \(\pi\), and \(\bar{\pi}\) is a prime element of \(\mathbb{Z}[i]\).

public theorem gaussianInt_split_conj {p : ℕ} [Fact p.Prime] {π : ℤ[i]}
    (hnorm : Zsqrtd.norm π = p) :
    (p : ℤ[i]) = π * star π ∧ Prime (star π)

Uses 1 · Used by 1

Proof usesGaussian integers of prime norm are prime

Used byNumber of Gaussian integers of norm a power of a split prime

TheoremGaussian integers of split prime norm are not associate to their conjugates#✓fully proved

Write \(N(a + bi) = a^2 + b^2\) for the norm on \(\mathbb{Z}[i]\). Let \(p\) be a prime with \(p \equiv 1 \pmod 4\) and let \(\pi \in \mathbb{Z}[i]\) satisfy \(N(\pi) = p\). Then the complex conjugate \(\bar{\pi}\) is not associated to \(\pi\): there is no unit \(u\) of \(\mathbb{Z}[i]\) with \(\bar{\pi} u = \pi\).

public theorem gaussianInt_split_nonassociated {p : ℕ} [Fact p.Prime] {π : ℤ[i]}
    (hnorm : Zsqrtd.norm π = p) (h1 : p % 4 = 1) :
    ¬ Associated (star π) π

Uses 1 · Used by 1

Proof usesUnits of the Gaussian integers

Used byNumber of Gaussian integers of norm a power of a split prime

TheoremNumber of Gaussian integers of norm a power of a split prime#✓fully proved

Write \(N(a + bi) = a^2 + b^2\) for the norm on \(\mathbb{Z}[i]\). Let \(p\) be a prime with \(p \equiv 1 \pmod 4\), let \(e\) be a natural number, and suppose \(\pi \in \mathbb{Z}[i]\) is a prime element with \(N(\pi) = p\). Then exactly \(4(e + 1)\) Gaussian integers \(\alpha\) satisfy \(|N(\alpha)| = p^e\).

public theorem gaussianInt_card_repr_prime_pow {p e : ℕ} [Fact p.Prime]
    (h1 : p % 4 = 1) {π : ℤ[i]} (hnorm : Zsqrtd.norm π = p)
    (hprime : Prime π) :
    Fintype.card {α : ℤ[i] // (Zsqrtd.norm α).natAbs = p ^ e} = 4 * (e + 1)

Uses 8 · Used by 1

Proof usesFactoring a prime as a Gaussian integer times its conjugate · Gaussian integers of split prime norm are not associate to their conjugates · Enumeration of the Gaussian units · Inverses of the Gaussian units · The enumeration of the Gaussian units is complete · The four Gaussian units are distinct · Each Gaussian unit times its listed inverse is one · Norm counts at a split prime

Used byJacobi's two-square theorem

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.