Documentation

Mathlib.NumberTheory.LegendreSymbol.ZModChar

Quadratic characters on ℤ/nℤ #

This file defines some quadratic characters on the rings ℤ/4ℤ and ℤ/8ℤ.

We set them up to be of type MulChar (ZMod n) ℤ, where n is 4 or 8.

Tags #

quadratic character, zmod

Quadratic characters mod 4 and 8 #

We define the primitive quadratic characters χ₄on ZMod 4 and χ₈, χ₈' on ZMod 8.

@[simp]
theorem ZMod.χ₄_apply (a : ZMod 4) :
ZMod.χ₄ a = match a with | 0 => 0 | 2 => 0 | 1 => 1 | 3 => -1

Define the nontrivial quadratic character on ZMod 4, χ₄. It corresponds to the extension ℚ(√-1)/ℚ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem ZMod.isQuadratic_χ₄ :
    ZMod.χ₄.IsQuadratic

    χ₄ takes values in {0, 1, -1}

    theorem ZMod.χ₄_nat_mod_four (n : ) :
    ZMod.χ₄ n = ZMod.χ₄ (n % 4)

    The value of χ₄ n, for n : ℕ, depends only on n % 4.

    theorem ZMod.χ₄_int_mod_four (n : ) :
    ZMod.χ₄ n = ZMod.χ₄ (n % 4)

    The value of χ₄ n, for n : ℤ, depends only on n % 4.

    theorem ZMod.χ₄_int_eq_if_mod_four (n : ) :
    ZMod.χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

    An explicit description of χ₄ on integers / naturals

    theorem ZMod.χ₄_nat_eq_if_mod_four (n : ) :
    ZMod.χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
    theorem ZMod.χ₄_eq_neg_one_pow {n : } (hn : n % 2 = 1) :
    ZMod.χ₄ n = (-1) ^ (n / 2)

    Alternative description of χ₄ n for odd n : ℕ in terms of powers of -1

    theorem ZMod.χ₄_nat_one_mod_four {n : } (hn : n % 4 = 1) :
    ZMod.χ₄ n = 1

    If n % 4 = 1, then χ₄ n = 1.

    theorem ZMod.χ₄_nat_three_mod_four {n : } (hn : n % 4 = 3) :
    ZMod.χ₄ n = -1

    If n % 4 = 3, then χ₄ n = -1.

    theorem ZMod.χ₄_int_one_mod_four {n : } (hn : n % 4 = 1) :
    ZMod.χ₄ n = 1

    If n % 4 = 1, then χ₄ n = 1.

    theorem ZMod.χ₄_int_three_mod_four {n : } (hn : n % 4 = 3) :
    ZMod.χ₄ n = -1

    If n % 4 = 3, then χ₄ n = -1.

    theorem ZMod.neg_one_pow_div_two_of_one_mod_four {n : } (hn : n % 4 = 1) :
    (-1) ^ (n / 2) = 1

    If n % 4 = 1, then (-1)^(n/2) = 1.

    theorem ZMod.neg_one_pow_div_two_of_three_mod_four {n : } (hn : n % 4 = 3) :
    (-1) ^ (n / 2) = -1

    If n % 4 = 3, then (-1)^(n/2) = -1.

    @[simp]
    theorem ZMod.χ₈_apply (a : ZMod 8) :
    ZMod.χ₈ a = match a with | 0 => 0 | 2 => 0 | 4 => 0 | 6 => 0 | 1 => 1 | 7 => 1 | 3 => -1 | 5 => -1

    Define the first primitive quadratic character on ZMod 8, χ₈. It corresponds to the extension ℚ(√2)/ℚ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem ZMod.isQuadratic_χ₈ :
      ZMod.χ₈.IsQuadratic

      χ₈ takes values in {0, 1, -1}

      theorem ZMod.χ₈_nat_mod_eight (n : ) :
      ZMod.χ₈ n = ZMod.χ₈ (n % 8)

      The value of χ₈ n, for n : ℕ, depends only on n % 8.

      theorem ZMod.χ₈_int_mod_eight (n : ) :
      ZMod.χ₈ n = ZMod.χ₈ (n % 8)

      The value of χ₈ n, for n : ℤ, depends only on n % 8.

      theorem ZMod.χ₈_int_eq_if_mod_eight (n : ) :
      ZMod.χ₈ n = if n % 2 = 0 then 0 else if n % 8 = 1 n % 8 = 7 then 1 else -1

      An explicit description of χ₈ on integers / naturals

      theorem ZMod.χ₈_nat_eq_if_mod_eight (n : ) :
      ZMod.χ₈ n = if n % 2 = 0 then 0 else if n % 8 = 1 n % 8 = 7 then 1 else -1
      @[simp]
      theorem ZMod.χ₈'_apply (a : ZMod 8) :
      ZMod.χ₈' a = match a with | 0 => 0 | 2 => 0 | 4 => 0 | 6 => 0 | 1 => 1 | 3 => 1 | 5 => -1 | 7 => -1

      Define the second primitive quadratic character on ZMod 8, χ₈'. It corresponds to the extension ℚ(√-2)/ℚ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        χ₈' takes values in {0, 1, -1}

        theorem ZMod.χ₈'_int_eq_if_mod_eight (n : ) :
        ZMod.χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 n % 8 = 3 then 1 else -1

        An explicit description of χ₈' on integers / naturals

        theorem ZMod.χ₈'_nat_eq_if_mod_eight (n : ) :
        ZMod.χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 n % 8 = 3 then 1 else -1
        theorem ZMod.χ₈'_eq_χ₄_mul_χ₈ (a : ZMod 8) :
        ZMod.χ₈' a = ZMod.χ₄ a.cast * ZMod.χ₈ a

        The relation between χ₄, χ₈ and χ₈'

        theorem ZMod.χ₈'_int_eq_χ₄_mul_χ₈ (a : ) :
        ZMod.χ₈' a = ZMod.χ₄ a * ZMod.χ₈ a