Imaginary quadratic discriminants

19 fully proved

Imaginary Quadratic Discriminant

DefinitionImaginary quadratic discriminant#✓fully proved

An integer \(D\) is an imaginary quadratic discriminant if \(D < 0\) and either \(D \equiv 0 \pmod 4\) or \(D \equiv 1 \pmod 4\).

def IsImaginaryQuadraticDiscriminant (D : Int) : Prop :=
  D < 0 ∧ (D % 4 = 0 ∨ D % 4 = 1)

Used by 8

Used byImaginary quadratic discriminants · Fundamental imaginary quadratic discriminants are imaginary quadratic discriminants · Characterization of imaginary quadratic discriminants · Criterion for an imaginary quadratic discriminant · Imaginary quadratic discriminants are congruent to 0 or 1 mod 4 · Imaginary quadratic discriminants are negative · Negative multiples of 4 are imaginary quadratic discriminants · Negative integers congruent to 1 mod 4 are imaginary quadratic discriminants

DefinitionFundamental imaginary quadratic discriminant#✓fully proved

An integer \(D\) is a fundamental imaginary quadratic discriminant if \(D < 0\) and \(D\) is a fundamental discriminant.

def IsFundamentalImaginaryQuadraticDiscriminant (D : Int) : Prop :=
  D < 0 ∧ MetaMathlibExt.IsFundamentalDiscriminant D

Uses 1 · Used by 8

Statement usesFundamental discriminant

Used byFundamental imaginary quadratic discriminants · Conductor decomposition of an imaginary quadratic discriminant · The fundamental part of a conductor decomposition · Characterization of fundamental imaginary quadratic discriminants · Negative fundamental discriminants are fundamental imaginary quadratic discriminants · Fundamental imaginary quadratic discriminants are fundamental discriminants · Fundamental imaginary quadratic discriminants are imaginary quadratic discriminants · Decomposition from a conductor and a fundamental discriminant

DefinitionImaginary quadratic discriminants#✓fully proved

The set of imaginary quadratic discriminants is the set of integers \(D\) such that \(D < 0\) and \(D\) is congruent to \(0\) or \(1\) modulo \(4\).

def imaginaryQuadraticDiscriminants : Set Int :=
  {D | IsImaginaryQuadraticDiscriminant D}

Uses 1

Statement usesImaginary quadratic discriminant

DefinitionFundamental imaginary quadratic discriminants#✓fully proved

The set of fundamental imaginary quadratic discriminants is the set of integers \(D\) with \(D < 0\) that are fundamental discriminants.

def fundamentalImaginaryQuadraticDiscriminants : Set Int :=
  {D | IsFundamentalImaginaryQuadraticDiscriminant D}

Uses 1

Statement usesFundamental imaginary quadratic discriminant

StructureConductor decomposition of an imaginary quadratic discriminant#✓fully proved

For an integer \(D\), a decomposition of \(D\) consists of integers \(u\) and \(D_K\) such that \(u \ge 1\), \(D_K\) is a fundamental imaginary quadratic discriminant, and \(D = u^2 D_K\). The integer \(u\) is called the conductor.

structure ImaginaryQuadraticDiscriminantDecomposition (D : Int) where
  u : Int
  D_K : Int
  hu : u ≥ 1
  hD_K : IsFundamentalImaginaryQuadraticDiscriminant D_K
  hD : D = u ^ 2 * D_K

Uses 1 · Used by 4

Statement usesFundamental imaginary quadratic discriminant

Used byThe fundamental part of a conductor decomposition · Decomposition from a conductor and a fundamental discriminant · The equation of a discriminant decomposition · The conductor of a discriminant decomposition is at least one

TheoremCharacterization of imaginary quadratic discriminants#✓fully proved

An integer \(D\) is an imaginary quadratic discriminant if and only if \(D < 0\) and \(D\) is congruent to \(0\) or \(1\) modulo \(4\).

theorem isImaginaryQuadraticDiscriminant_iff (D : Int) :
    IsImaginaryQuadraticDiscriminant D ↔ D < 0 ∧ (D % 4 = 0 ∨ D % 4 = 1)

Uses 1

Statement usesImaginary quadratic discriminant

TheoremCriterion for an imaginary quadratic discriminant#✓fully proved

If an integer \(D\) satisfies \(D < 0\) and either \(D \equiv 0 \pmod 4\) or \(D \equiv 1 \pmod 4\), then \(D\) is an imaginary quadratic discriminant.

theorem isImaginaryQuadraticDiscriminant_mk {D : Int} (hneg : D < 0)
    (hmod : D % 4 = 0 ∨ D % 4 = 1) : IsImaginaryQuadraticDiscriminant D

Uses 1

Statement usesImaginary quadratic discriminant

TheoremImaginary quadratic discriminants are negative#✓fully proved

Every imaginary quadratic discriminant \(D\) satisfies \(D < 0\).

theorem isImaginaryQuadraticDiscriminant_neg {D : Int}
    (h : IsImaginaryQuadraticDiscriminant D) : D < 0

Uses 1

Statement usesImaginary quadratic discriminant

TheoremImaginary quadratic discriminants are congruent to 0 or 1 mod 4#✓fully proved

Every imaginary quadratic discriminant \(D\) satisfies \(D \equiv 0 \pmod 4\) or \(D \equiv 1 \pmod 4\).

theorem isImaginaryQuadraticDiscriminant_mod {D : Int}
    (h : IsImaginaryQuadraticDiscriminant D) : D % 4 = 0 ∨ D % 4 = 1

Uses 1

Statement usesImaginary quadratic discriminant

TheoremNegative multiples of 4 are imaginary quadratic discriminants#✓fully proved

If an integer \(D\) satisfies \(D < 0\) and \(D \equiv 0 \pmod 4\), then \(D\) is an imaginary quadratic discriminant.

theorem isImaginaryQuadraticDiscriminant_of_mod_zero {D : Int} (hneg : D < 0)
    (hmod : D % 4 = 0) : IsImaginaryQuadraticDiscriminant D

Uses 1

Statement usesImaginary quadratic discriminant

TheoremNegative integers congruent to 1 mod 4 are imaginary quadratic discriminants#✓fully proved

If an integer \(D\) satisfies \(D < 0\) and \(D \equiv 1 \pmod 4\), then \(D\) is an imaginary quadratic discriminant.

theorem isImaginaryQuadraticDiscriminant_of_mod_one {D : Int} (hneg : D < 0)
    (hmod : D % 4 = 1) : IsImaginaryQuadraticDiscriminant D

Uses 1

Statement usesImaginary quadratic discriminant

TheoremCharacterization of fundamental imaginary quadratic discriminants#✓fully proved

An integer \(D\) is a fundamental imaginary quadratic discriminant if and only if \(D < 0\) and \(D\) is a fundamental discriminant.

theorem isFundamentalImaginaryQuadraticDiscriminant_iff (D : Int) :
    IsFundamentalImaginaryQuadraticDiscriminant D ↔
      D < 0 ∧ MetaMathlibExt.IsFundamentalDiscriminant D

Uses 2

Statement usesFundamental imaginary quadratic discriminant · Fundamental discriminant

TheoremNegative fundamental discriminants are fundamental imaginary quadratic discriminants#✓fully proved

If an integer \(D\) satisfies \(D < 0\) and is a fundamental discriminant, then \(D\) is a fundamental imaginary quadratic discriminant.

theorem isFundamentalImaginaryQuadraticDiscriminant_mk {D : Int} (hneg : D < 0)
    (hfund : MetaMathlibExt.IsFundamentalDiscriminant D) :
    IsFundamentalImaginaryQuadraticDiscriminant D

Uses 2

Statement usesFundamental imaginary quadratic discriminant · Fundamental discriminant

TheoremFundamental imaginary quadratic discriminants are fundamental discriminants#✓fully proved

Every fundamental imaginary quadratic discriminant \(D\) is a fundamental discriminant.

theorem isFundamentalImaginaryQuadraticDiscriminant_isFundamentalDiscriminant {D : Int}
    (h : IsFundamentalImaginaryQuadraticDiscriminant D) :
    MetaMathlibExt.IsFundamentalDiscriminant D

Uses 2

Statement usesFundamental imaginary quadratic discriminant · Fundamental discriminant

TheoremFundamental imaginary quadratic discriminants are imaginary quadratic discriminants#✓fully proved

Every fundamental imaginary quadratic discriminant is an imaginary quadratic discriminant.

theorem isFundamentalImaginaryQuadraticDiscriminant_isImaginary {D : Int}
    (h : IsFundamentalImaginaryQuadraticDiscriminant D) :
    IsImaginaryQuadraticDiscriminant D

Uses 3

Statement usesFundamental imaginary quadratic discriminant · Imaginary quadratic discriminant

Proof usesFundamental discriminant

Imaginary Quadratic Discriminant Decomposition

TheoremThe fundamental part of a conductor decomposition#✓fully proved

For every conductor decomposition of an integer \(D\), consisting of an integer \(u \ge 1\) and a fundamental imaginary quadratic discriminant \(D_K\) with \(D = u^2 D_K\), the integer \(D_K\) is a fundamental imaginary quadratic discriminant.

theorem isFundamental (h : ImaginaryQuadraticDiscriminantDecomposition D) :
    IsFundamentalImaginaryQuadraticDiscriminant h.D_K

Uses 2

Statement usesConductor decomposition of an imaginary quadratic discriminant · Fundamental imaginary quadratic discriminant

TheoremThe conductor of a discriminant decomposition is at least one#✓fully proved

For every decomposition of an integer \(D\) into a conductor \(u\) and a fundamental imaginary quadratic discriminant \(D_K\), we have \(u \ge 1\).

theorem u_ge_one (h : ImaginaryQuadraticDiscriminantDecomposition D) : h.u ≥ 1

Uses 1

Statement usesConductor decomposition of an imaginary quadratic discriminant

TheoremThe equation of a discriminant decomposition#✓fully proved

For every decomposition of an integer \(D\) into a conductor \(u\) and a fundamental imaginary quadratic discriminant \(D_K\), we have \(D = u^2 D_K\).

theorem prop_eq (h : ImaginaryQuadraticDiscriminantDecomposition D) :
    D = h.u ^ 2 * h.D_K

Uses 1

Statement usesConductor decomposition of an imaginary quadratic discriminant

DefinitionDecomposition from a conductor and a fundamental discriminant#✓fully proved

Let \(D\) be an integer. If \(u \ge 1\) is an integer, \(D_K\) is a fundamental imaginary quadratic discriminant and \(D = u^2 D_K\), then \(u\) and \(D_K\) form a decomposition of \(D\) into the conductor \(u\) and the fundamental imaginary quadratic discriminant \(D_K\).

def ofFundamental (u D_K : Int) (hu : u ≥ 1)
    (hD_K : IsFundamentalImaginaryQuadraticDiscriminant D_K)
    (hD : D = u ^ 2 * D_K) : ImaginaryQuadraticDiscriminantDecomposition D :=
  ⟨u, D_K, hu, hD_K, hD⟩

Uses 2

Statement usesConductor decomposition of an imaginary quadratic discriminant · Fundamental imaginary quadratic discriminant

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.