Documentation

TauCeti.NumberTheory.Multiquadratic.Prime.Discriminant.Even

Even prime discriminants #

The prime discriminants are the fundamental discriminants divisible by exactly one prime: the odd ones p* = (-1)^((p - 1) / 2) p, developed in TauCeti.NumberTheory.Multiquadratic.Prime.Discriminant.Basic, and the three even ones treated here. Each even prime discriminant is four times a squarefree radicand:

The quotient D / 4 is the radicand whose square root generates the same quadratic field ℚ(√D). These are the 2-adic factors in the factorization of a fundamental discriminant into prime discriminants.

Main definitions and results #

source
def TauCeti.Multiquadratic.IsEvenPrimeDiscriminant (D : ℤ) :
Prop

The three even prime discriminants: -4, 8, and -8.

Instances For
    source
    theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_iff {D : ℤ} :
    IsEvenPrimeDiscriminant D ↔ D = -4 ∨ D = 8 ∨ D = -8

    The defining disjunction for IsEvenPrimeDiscriminant.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_neg_four :
    IsEvenPrimeDiscriminant (-4)
    source
    @[simp]
    theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_eight :
    IsEvenPrimeDiscriminant 8
    source
    @[simp]
    theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_neg_eight :
    IsEvenPrimeDiscriminant (-8)
    source
    def TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand (D : ℤ) :
    ℤ

    The squarefree radicand associated to an even prime discriminant. For D = -4, 8, -8 this gives respectively -1, 2, -2.

    Instances For
      source
      @[simp]
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_neg_four :
      evenPrimeDiscriminantRadicand (-4) = -1
      source
      @[simp]
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eight :
      evenPrimeDiscriminantRadicand 8 = 2
      source
      @[simp]
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_neg_eight :
      evenPrimeDiscriminantRadicand (-8) = -2
      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminant_eq_four_mul_radicand {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      D = 4 * evenPrimeDiscriminantRadicand D

      An even prime discriminant is four times its associated squarefree radicand.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_neg_one_or_eq_two_or_eq_neg_two {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      evenPrimeDiscriminantRadicand D = -1 ∨ evenPrimeDiscriminantRadicand D = 2 ∨ evenPrimeDiscriminantRadicand D = -2

      The associated squarefree radicand of an even prime discriminant is one of -1, 2, or -2.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_natAbs_eq_one_or_two {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      (evenPrimeDiscriminantRadicand D).natAbs = 1 ∨ (evenPrimeDiscriminantRadicand D).natAbs = 2

      The absolute value of the radicand attached to an even prime discriminant is 1 or 2.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_ne_zero {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      evenPrimeDiscriminantRadicand D ≠ 0

      The radicand attached to an even prime discriminant is nonzero.

      source
      theorem TauCeti.Multiquadratic.squarefree_evenPrimeDiscriminantRadicand {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      Squarefree (evenPrimeDiscriminantRadicand D)

      The radicand attached to an even prime discriminant is squarefree.

      source
      theorem TauCeti.Multiquadratic.two_dvd_evenPrimeDiscriminant {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      2 ∣ D

      The even prime discriminants themselves are even.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_mod_four_eq_three_or_two {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      evenPrimeDiscriminantRadicand D % 4 = 3 ∨ evenPrimeDiscriminantRadicand D % 4 = 2

      The radicand attached to an even prime discriminant is congruent to -1 or 2 modulo 4.

      source
      theorem TauCeti.Multiquadratic.not_isSquare_evenPrimeDiscriminantRadicand_rat {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      ¬IsSquare ↑(evenPrimeDiscriminantRadicand D)

      The rational radicand associated to an even prime discriminant is not a square.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_neg_one_iff {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      evenPrimeDiscriminantRadicand D = -1 ↔ D = -4

      The discriminant -4 gives the radicand -1.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_two_iff {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      evenPrimeDiscriminantRadicand D = 2 ↔ D = 8

      The discriminant 8 gives the radicand 2.

      source
      theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_neg_two_iff {D : ℤ} (hD : IsEvenPrimeDiscriminant D) :
      evenPrimeDiscriminantRadicand D = -2 ↔ D = -8

      The discriminant -8 gives the radicand -2.