mathlib documentation

number_theory.legendre_symbol.zmod_char

Quadratic characters on ℤ/nℤ #

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

Tags #

quadratic character, zmod

Quadratic characters mod 4 and 8 #

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

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

Equations
@[simp]
theorem zmod.χ₄_apply (ᾰ : fin (2.add (1.add 0)).succ) :
zmod.χ₄ = ![0, 1, 0, -1]

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

theorem zmod.χ₄_int_eq_if_mod_four (n : ) :
zmod.χ₄ n = ite (n % 2 = 0) 0 (ite (n % 4 = 1) 1 (-1))

An explicit description of χ₄ on integers / naturals

theorem zmod.χ₄_nat_eq_if_mod_four (n : ) :
zmod.χ₄ n = ite (n % 2 = 0) 0 (ite (n % 4 = 1) 1 (-1))
theorem zmod.χ₄_eq_neg_one_pow {n : } (hn : n % 2 = 1) :
zmod.χ₄ n = (-1) ^ (n / 2)

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

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

Equations
@[simp]
theorem zmod.χ₈_apply (ᾰ : fin (4.add (2.add (1.add 0))).succ) :
zmod.χ₈ = ![0, 1, 0, -1, 0, -1, 0, 1]

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

theorem zmod.χ₈_int_eq_if_mod_eight (n : ) :
zmod.χ₈ n = ite (n % 2 = 0) 0 (ite (n % 8 = 1 n % 8 = 7) 1 (-1))

An explicit description of χ₈ on integers / naturals

theorem zmod.χ₈_nat_eq_if_mod_eight (n : ) :
zmod.χ₈ n = ite (n % 2 = 0) 0 (ite (n % 8 = 1 n % 8 = 7) 1 (-1))
@[simp]
theorem zmod.χ₈'_apply (ᾰ : fin (4.add (2.add (1.add 0))).succ) :
zmod.χ₈' = ![0, 1, 0, 1, 0, -1, 0, -1]

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

Equations

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

theorem zmod.χ₈'_int_eq_if_mod_eight (n : ) :
zmod.χ₈' n = ite (n % 2 = 0) 0 (ite (n % 8 = 1 n % 8 = 3) 1 (-1))

An explicit description of χ₈' on integers / naturals

theorem zmod.χ₈'_nat_eq_if_mod_eight (n : ) :
zmod.χ₈' n = ite (n % 2 = 0) 0 (ite (n % 8 = 1 n % 8 = 3) 1 (-1))

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