Norms in imaginary quadratic integer rings

TheoremElements of \(\mathbb{Z}(\sqrt{d})\) of prime norm are prime#✓fully proved

Let \(d\) be an integer such that the ring \(\mathbb{Z}[\sqrt{d}]\) of formal expressions \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) and \(\sqrt{d}^2 = d\) is a unique factorization domain, with norm \(N(a + b\sqrt{d}) = a^2 - db^2\). If \(\pi \in \mathbb{Z}[\sqrt{d}]\) and \(|N(\pi)|\) is a prime number, then \(\pi\) is prime in \(\mathbb{Z}[\sqrt{d}]\).

public theorem prime_of_natAbs_norm_prime [UniqueFactorizationMonoid (ℤ√d)]
    {π : ℤ√d} (h : (Zsqrtd.norm π).natAbs.Prime) : Prime π

Used by 2

Used byGaussian integers of prime norm are prime · Elements of ℤ(√−2) of prime norm are prime

TheoremThe norm respects divisibility in \(\mathbb{Z}(\sqrt{d})\)#✓fully proved

Let \(d\) be an integer and let \(N(a + b\sqrt{d}) = a^2 - db^2\) be the norm on the ring \(\mathbb{Z}[\sqrt{d}]\) of formal expressions \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) and \(\sqrt{d}^2 = d\). If \(x\) divides \(y\) in \(\mathbb{Z}[\sqrt{d}]\), then \(|N(x)|\) divides \(|N(y)|\).

public theorem natAbs_norm_dvd_of_dvd {a b : ℤ√d} (h : a ∣ b) :
    (Zsqrtd.norm a).natAbs ∣ (Zsqrtd.norm b).natAbs

Used by 3

Used byCancelling a factor of coprime norm · Splitting an element along coprime norms · Primes of \(\mathbb{Z}(\sqrt{d})\) have prime-power norm

TheoremOnly zero has norm zero in \(\mathbb{Z}(\sqrt d)\) for \(d < 0\)#✓fully proved

Let \(d < 0\) be an integer and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm on the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)). If \(\alpha \in \mathbb{Z}[\sqrt d]\) satisfies \(|N(\alpha)| = 0\), then \(\alpha = 0\).

public theorem eq_zero_of_norm_natAbs_eq_zero (hd : d < 0) {x : ℤ√d}
    (h : (Zsqrtd.norm x).natAbs = 0) : x = 0

Used by 2

Used byCancelling a factor of coprime norm · Primes of \(\mathbb{Z}(\sqrt{d})\) have prime-power norm

TheoremCancelling a factor of coprime norm#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Let \(u\) and \(v\) be coprime natural numbers with \(u \ne 0\). If \(\beta, \beta_0, \gamma \in \mathbb{Z}[\sqrt d]\) satisfy \(|N(\beta)| \mid u\), \(|N(\gamma)| = v\) and \(\beta \mid \beta_0\gamma\), then \(\beta \mid \beta_0\).

public theorem dvd_of_coprime_norms [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    (hd : d < 0) {u v : ℕ} (huv : Nat.Coprime u v)
    (hu : u ≠ 0) :
    ∀ (m : ℕ) (β' : ℤ√d),
      (Zsqrtd.norm β').natAbs = m → m ∣ u →
      ∀ (β₀' γ₀ : ℤ√d), (Zsqrtd.norm γ₀).natAbs = v →
        β' ∣ β₀' * γ₀ → β' ∣ β₀'

Uses 2 · Used by 1

Proof usesOnly zero has norm zero in \(\mathbb{Z}(\sqrt d)\) for \(d < 0\) · The norm respects divisibility in \(\mathbb{Z}(\sqrt{d})\)

Used byNorm counts are multiplicative up to units

TheoremPrimes of \(\mathbb{Z}(\sqrt{d})\) have prime-power norm#✓fully proved

Let \(d < 0\) be an integer and let \(N(a + b\sqrt{d}) = a^2 - db^2\) be the norm on the ring \(\mathbb{Z}[\sqrt{d}]\) of numbers \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\). For every prime \(\varpi\) of \(\mathbb{Z}[\sqrt{d}]\) there are a prime number \(\ell\) and a natural number \(s \ne 0\) such that \(|N(\varpi)| = \ell^s\) and \(\varpi\) divides \(\ell\) in \(\mathbb{Z}[\sqrt{d}]\).

public theorem prime_pow_norm_of_prime (hd : d < 0) {ϖ : ℤ√d} (hprime : Prime ϖ) :
    ∃ ℓ s : ℕ, ℓ.Prime ∧ s ≠ 0 ∧ (Zsqrtd.norm ϖ).natAbs = ℓ ^ s ∧
      ϖ ∣ (ℓ : ℤ√d)

Uses 2 · Used by 1

Proof usesOnly zero has norm zero in \(\mathbb{Z}(\sqrt d)\) for \(d < 0\) · The norm respects divisibility in \(\mathbb{Z}(\sqrt{d})\)

Used bySplitting an element along coprime norms

TheoremSplitting an element along coprime norms#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Let \(u\) and \(v\) be coprime nonzero natural numbers. Every \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = uv\) factors as \(\alpha = \beta\gamma\) with \(|N(\beta)| = u\) and \(|N(\gamma)| = v\).

public theorem exists_factor_of_coprime [UniqueFactorizationMonoid (ℤ√d)]
    (hd : d < 0) {u v : ℕ} (huv : Nat.Coprime u v)
    (hu : u ≠ 0) (hv : v ≠ 0) (α : ℤ√d)
    (hα : (Zsqrtd.norm α).natAbs = u * v) :
    ∃ β γ : ℤ√d, β * γ = α ∧ (Zsqrtd.norm β).natAbs = u ∧
      (Zsqrtd.norm γ).natAbs = v

Uses 2 · Used by 1

Proof usesThe norm respects divisibility in \(\mathbb{Z}(\sqrt{d})\) · Primes of \(\mathbb{Z}(\sqrt{d})\) have prime-power norm

Used byNorm counts are multiplicative up to units

TheoremCounting a norm class generated by one element#✓fully proved

Let \(d\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of formal sums \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is an integral domain with exactly \(k\) units, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Assume that for each \(m \in \mathbb{N}\) the set of \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = m\) is finite. Let \(n \in \mathbb{N}\) and let \(s \ne 0\) satisfy \(|N(s)| = n\). If every \(\alpha\) with \(|N(\alpha)| = n\) equals \(us\) for some unit \(u\), then exactly \(k\) elements \(\alpha\) satisfy \(|N(\alpha)| = n\).

public theorem card_repr_of_shape [IsDomain (ℤ√d)]
    [∀ n : ℕ, Fintype {α : ℤ√d // (Zsqrtd.norm α).natAbs = n}]
    {k : ℕ} (unitVal unitValInv : Fin k → ℤ√d)
    (hinv : ∀ i, unitVal i * unitValInv i = 1) (hinj : Function.Injective unitVal)
    (hcomplete : ∀ u : ℤ√d, IsUnit u → ∃ i, unitVal i = u) {n : ℕ} (s : ℤ√d)
    (hs : (Zsqrtd.norm s).natAbs = n) (hs0 : s ≠ 0)
    (hclass : ∀ α : ℤ√d, (Zsqrtd.norm α).natAbs = n →
      ∃ u : ℤ√d, IsUnit u ∧ α = u * s) :
    Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = n} = k

Used by 4

Used byNorm counts determined by prime powers · Norm counts at an inert prime · Norm counts at powers of a ramified two · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\)

TheoremNorm counts are multiplicative up to units#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain with exactly \(k\) units, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Assume that for each \(n \in \mathbb{N}\) the set of \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = n\) is finite, and let \(r(n)\) be its size. If \(u\) and \(v\) are coprime nonzero natural numbers, then \(r(u)\,r(v) = k\,r(uv)\).

public theorem card_mul_of_coprime [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    [∀ n : ℕ, Fintype {α : ℤ√d // (Zsqrtd.norm α).natAbs = n}]
    (hd : d < 0) {k : ℕ} (unitVal unitValInv : Fin k → ℤ√d)
    (hinv : ∀ i, unitVal i * unitValInv i = 1) (hinj : Function.Injective unitVal)
    (hcomplete : ∀ u : ℤ√d, IsUnit u → ∃ i, unitVal i = u) {u v : ℕ} (huv : Nat.Coprime u v)
    (hu : u ≠ 0) (hv : v ≠ 0) :
    Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = u} *
      Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = v}
      = k * Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = u * v}

Uses 2 · Used by 1

Proof usesCancelling a factor of coprime norm · Splitting an element along coprime norms

Used byNorm counts determined by prime powers

TheoremThe norm of a power in \(\mathbb{Z}(\sqrt{d})\)#✓fully proved

Let \(d\) be an integer and let \(N(a + b\sqrt{d}) = a^2 - db^2\) be the norm on the ring \(\mathbb{Z}[\sqrt{d}]\) of formal expressions \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) and \(\sqrt{d}^2 = d\). Then \(N(x^n) = N(x)^n\) for every \(x \in \mathbb{Z}[\sqrt{d}]\) and every natural number \(n\).

public theorem norm_pow (x : ℤ√d) (n : ℕ) : Zsqrtd.norm (x ^ n) = Zsqrtd.norm x ^ n

Used by 1

Used byNorm counts at powers of a ramified two

TheoremElements whose norm is a power of a ramified two#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Suppose \(2 = \varepsilon\rho^2\) for a unit \(\varepsilon\) and a prime \(\rho\) with \(|N(\rho)| = 2\). Then for every \(e \in \mathbb{N}\), every \(\alpha\) with \(|N(\alpha)| = 2^e\) equals \(u\rho^e\) for some unit \(u\).

public theorem exists_unit_mul_pow_of_norm_two_pow
    [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    (hd : d < 0) {ρ ε : ℤ√d} (hρ : Prime ρ) (hρnorm : (Zsqrtd.norm ρ).natAbs = 2)
    (hε : IsUnit ε) (htwo : (2 : ℤ√d) = ε * ρ ^ 2) (e : ℕ) (α : ℤ√d)
    (hα : (Zsqrtd.norm α).natAbs = 2 ^ e) :
    ∃ u : ℤ√d, IsUnit u ∧ α = u * ρ ^ e

Used by 1

Used byNorm counts at powers of a ramified two

TheoremNorm counts at powers of a ramified two#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain with exactly \(k\) units, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Assume that for each \(n \in \mathbb{N}\) the set of \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = n\) is finite, and let \(r(n)\) be its size. If \(2 = \varepsilon\rho^2\) for a unit \(\varepsilon\) and a prime \(\rho\) with \(|N(\rho)| = 2\), then \(r(2^e) = k\) for every \(e \in \mathbb{N}\).

public theorem card_norm_two_pow [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    [∀ n : ℕ, Fintype {α : ℤ√d // (Zsqrtd.norm α).natAbs = n}]
    (hd : d < 0) {k : ℕ} (unitVal unitValInv : Fin k → ℤ√d)
    (hinv : ∀ i, unitVal i * unitValInv i = 1) (hinj : Function.Injective unitVal)
    (hcomplete : ∀ u : ℤ√d, IsUnit u → ∃ i, unitVal i = u) {ρ ε : ℤ√d} (hρ : Prime ρ)
    (hρnorm : (Zsqrtd.norm ρ).natAbs = 2) (hε : IsUnit ε) (htwo : (2 : ℤ√d) = ε * ρ ^ 2)
    (e : ℕ) : Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = 2 ^ e} = k

Uses 3 · Used by 2

Proof usesCounting a norm class generated by one element · Elements whose norm is a power of a ramified two · The norm of a power in \(\mathbb{Z}(\sqrt{d})\)

Used byJacobi's two-square theorem · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\)

TheoremPeeling an inert prime off an element of norm \(q^f\)#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt{d}]\) of numbers \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) is a unique factorization domain, with norm \(N(a + b\sqrt{d}) = a^2 - db^2\). Let \(q\) be a natural number that is prime in \(\mathbb{Z}[\sqrt{d}]\), let \(f\) be a natural number, and let \(\alpha \in \mathbb{Z}[\sqrt{d}]\) be nonzero and not a unit with \(|N(\alpha)| = q^f\). Then \(\alpha = wq\beta\) for some unit \(w\) and some \(\beta \in \mathbb{Z}[\sqrt{d}]\) with \(q^2 \cdot |N(\beta)| = q^f\).

public theorem inert_peel [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)] {q : ℕ}
    (hd : d < 0) (hqprime : Prime (q : ℤ√d))
    {f : ℕ} {α : ℤ√d} (hα : (Zsqrtd.norm α).natAbs = q ^ f)
    (hαnu : ¬ IsUnit α) (hα0 : α ≠ 0) :
    ∃ β : ℤ√d, ∃ w : (ℤ√d)ˣ, α = (w : ℤ√d) * (q : ℤ√d) * β ∧
      (q * q) * (Zsqrtd.norm β).natAbs = q ^ f

Used by 2

Used byElements of norm \(q^{2n}\) over an inert prime · No element has norm \(q^{2n+1}\) over an inert prime

TheoremElements of norm \(q^{2n}\) over an inert prime#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt{d}]\) of numbers \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) is a unique factorization domain, with norm \(N(a + b\sqrt{d}) = a^2 - db^2\). Let \(q\) be a prime number that is also prime in \(\mathbb{Z}[\sqrt{d}]\). Then for every natural number \(n\), every \(\alpha \in \mathbb{Z}[\sqrt{d}]\) with \(|N(\alpha)| = q^{2n}\) is of the form \(\alpha = uq^n\) for some unit \(u\).

public theorem inert_even [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)] {q : ℕ} [Fact q.Prime]
    (hd : d < 0) (hqprime : Prime (q : ℤ√d))
    (n : ℕ) (α : ℤ√d) (hα : (Zsqrtd.norm α).natAbs = q ^ (2 * n)) :
    ∃ u : ℤ√d, IsUnit u ∧ α = u * (q : ℤ√d) ^ n

Uses 1 · Used by 1

Proof usesPeeling an inert prime off an element of norm \(q^f\)

Used byNorm counts at an inert prime

TheoremNo element has norm \(q^{2n+1}\) over an inert prime#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt{d}]\) of numbers \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) is a unique factorization domain, with norm \(N(a + b\sqrt{d}) = a^2 - db^2\). Let \(q\) be a prime number that is also prime in \(\mathbb{Z}[\sqrt{d}]\). Then for every natural number \(n\), no \(\alpha \in \mathbb{Z}[\sqrt{d}]\) satisfies \(|N(\alpha)| = q^{2n+1}\).

public theorem inert_odd [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)] {q : ℕ} [Fact q.Prime]
    (hd : d < 0) (hqprime : Prime (q : ℤ√d)) :
    ∀ (n : ℕ) (α : ℤ√d),
      (Zsqrtd.norm α).natAbs = q ^ (2 * n + 1) → False

Uses 1 · Used by 1

Proof usesPeeling an inert prime off an element of norm \(q^f\)

Used byNorm counts at an inert prime

TheoremNorm counts at an inert prime#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain with exactly \(k\) units, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Assume that for each \(n \in \mathbb{N}\) the set of \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = n\) is finite, and let \(r(n)\) be its size. If \(q\) is a prime number that is also a prime element of \(\mathbb{Z}[\sqrt d]\), then for every \(f \in \mathbb{N}\) we have \(r(q^f) = k\) when \(f\) is even and \(r(q^f) = 0\) when \(f\) is odd.

public theorem card_norm_inert_pow [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    [∀ n : ℕ, Fintype {α : ℤ√d // (Zsqrtd.norm α).natAbs = n}]
    (hd : d < 0) {k : ℕ} (unitVal unitValInv : Fin k → ℤ√d)
    (hinv : ∀ i, unitVal i * unitValInv i = 1) (hinj : Function.Injective unitVal)
    (hcomplete : ∀ u : ℤ√d, IsUnit u → ∃ i, unitVal i = u) {q f : ℕ} [Fact q.Prime]
    (hqprime : Prime (q : ℤ√d)) :
    Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = q ^ f} = if Even f then k else 0

Uses 3 · Used by 2

Proof usesCounting a norm class generated by one element · Elements of norm \(q^{2n}\) over an inert prime · No element has norm \(q^{2n+1}\) over an inert prime

Used byJacobi's two-square theorem · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime

TheoremElements of norm \(p^e\) over a split prime#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt{d}]\) of numbers \(a + b\sqrt{d}\) with \(a, b \in \mathbb{Z}\) is a unique factorization domain, with norm \(N(a + b\sqrt{d}) = a^2 - db^2\) and conjugation \(\overline{a + b\sqrt{d}} = a - b\sqrt{d}\). Let \(p\) be a prime number and let \(\pi\) be a prime of \(\mathbb{Z}[\sqrt{d}]\) with \(N(\pi) = p\) and \(p = \pi\bar{\pi}\) such that \(\bar{\pi}\) is also prime. Then for every natural number \(e\), every \(\alpha \in \mathbb{Z}[\sqrt{d}]\) with \(|N(\alpha)| = p^e\) is of the form \(\alpha = u\pi^j\bar{\pi}^k\) for some unit \(u\) and natural numbers \(j, k\) with \(j + k = e\).

public theorem exists_unit_mul_split_pow [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    (hd : d < 0) {p : ℕ} [Fact p.Prime]
    {π : ℤ√d} (hnorm : Zsqrtd.norm π = p) (hprime : Prime π)
    (hmul : (p : ℤ√d) = π * star π)
    (hπbar_prime : Prime (star π)) :
    ∀ (e' : ℕ) (α : ℤ√d),
      (Zsqrtd.norm α).natAbs = p ^ e' →
      ∃ u : ℤ√d,
        IsUnit u ∧ ∃ j k : ℕ, j + k = e' ∧ α = u * π ^ j * star π ^ k

Used by 1

Used byNorm counts at a split prime

TheoremNorm counts at a split prime#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain with exactly \(k\) units, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Assume that for each \(n \in \mathbb{N}\) the set of \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = n\) is finite, and let \(r(n)\) be its size. Let \(p\) be a prime number and \(\pi \in \mathbb{Z}[\sqrt d]\) with \(N(\pi) = p\) and \(p = \pi\bar\pi\), where \(\overline{a + b\sqrt d} = a - b\sqrt d\). If \(\pi\) and \(\bar\pi\) are prime and \(\bar\pi\) is not associated to \(\pi\), then \(r(p^e) = k(e + 1)\) for every \(e \in \mathbb{N}\).

public theorem card_norm_split_pow [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    [∀ n : ℕ, Fintype {α : ℤ√d // (Zsqrtd.norm α).natAbs = n}]
    (hd : d < 0) {k : ℕ} (unitVal unitValInv : Fin k → ℤ√d)
    (hinv : ∀ i, unitVal i * unitValInv i = 1) (hinj : Function.Injective unitVal)
    (hcomplete : ∀ u : ℤ√d, IsUnit u → ∃ i, unitVal i = u) {p e : ℕ} [Fact p.Prime] {π : ℤ√d}
    (hnorm : Zsqrtd.norm π = p) (hprime : Prime π) (hmul : (p : ℤ√d) = π * star π)
    (hπbar_prime : Prime (star π)) (hnassoc : ¬ Associated (star π) π) :
    Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = p ^ e} = k * (e + 1)

Uses 1 · Used by 2

Proof usesElements of norm \(p^e\) over a split prime

Used byNumber of Gaussian integers of norm a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime

TheoremNorm counts determined by prime powers#✓fully proved

Let \(d < 0\) be an integer such that the ring \(\mathbb{Z}[\sqrt d]\) of elements \(a + b\sqrt d\) (\(a, b \in \mathbb{Z}\)) is a unique factorization domain with exactly \(k\) units, and let \(N(a + b\sqrt d) = a^2 - db^2\) be the norm. Assume that for each \(n \in \mathbb{N}\) the set of \(\alpha \in \mathbb{Z}[\sqrt d]\) with \(|N(\alpha)| = n\) is finite, and let \(r(n)\) be its size. Let \(D : \mathbb{N} \to \mathbb{Z}\) satisfy \(D(1) = 1\) and \(D(mn) = D(m)\,D(n)\) for all coprime \(m, n\). If \(r(p^e) = k\,D(p^e)\) for every prime \(p\) and every \(e \ge 1\), then \(r(n) = k\,D(n)\) for every \(n \ne 0\).

public theorem card_norm_eq_mul_of_prime_pow [IsDomain (ℤ√d)] [UniqueFactorizationMonoid (ℤ√d)]
    [∀ n : ℕ, Fintype {α : ℤ√d // (Zsqrtd.norm α).natAbs = n}]
    (hd : d < 0) {k : ℕ} (unitVal unitValInv : Fin k → ℤ√d)
    (hinv : ∀ i, unitVal i * unitValInv i = 1) (hinj : Function.Injective unitVal)
    (hcomplete : ∀ u : ℤ√d, IsUnit u → ∃ i, unitVal i = u) {D : ℕ → ℤ} (hD1 : D 1 = 1)
    (hDmul : ∀ {m n : ℕ}, Nat.Coprime m n → D (m * n) = D m * D n)
    (hpp : ∀ {p e : ℕ}, p.Prime → 0 < e →
      (Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = p ^ e} : ℤ) = k * D (p ^ e))
    {n : ℕ} (hn : n ≠ 0) :
    (Fintype.card {α : ℤ√d // (Zsqrtd.norm α).natAbs = n} : ℤ) = k * D n

Uses 2 · Used by 2

Proof usesNorm counts are multiplicative up to units · Counting a norm class generated by one element

Used byJacobi's two-square theorem · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.