mathlib3 documentation

number_theory.legendre_symbol.zmod_char

Quadratic characters on ℤ/nℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We set them up to be of type mul_char (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.

source
def zmod.χ₄  :
mul_char (zmod 4) ℤ

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

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

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

source
theorem zmod.χ₄_nat_mod_four (n : ℕ) :
⇑zmod.χ₄ ↑n = ⇑zmod.χ₄ ↑(n % 4)

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

source
theorem zmod.χ₄_int_mod_four (n : ℤ) :
⇑zmod.χ₄ ↑n = ⇑zmod.χ₄ ↑(n % 4)

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

source
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

source
theorem zmod.χ₄_nat_eq_if_mod_four (n : ℕ) :
⇑zmod.χ₄ ↑n = ite (n % 2 = 0) 0 (ite (n % 4 = 1) 1 (-1))
source
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

source
theorem zmod.χ₄_nat_one_mod_four {n : ℕ} (hn : n % 4 = 1) :
⇑zmod.χ₄ ↑n = 1

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

source
theorem zmod.χ₄_nat_three_mod_four {n : ℕ} (hn : n % 4 = 3) :
⇑zmod.χ₄ ↑n = -1

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

source
theorem zmod.χ₄_int_one_mod_four {n : ℤ} (hn : n % 4 = 1) :
⇑zmod.χ₄ ↑n = 1

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

source
theorem zmod.χ₄_int_three_mod_four {n : ℤ} (hn : n % 4 = 3) :
⇑zmod.χ₄ ↑n = -1

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

source
theorem 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.

source
theorem 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.

source
def zmod.χ₈  :
mul_char (zmod 8) ℤ

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

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

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

source
theorem zmod.χ₈_nat_mod_eight (n : ℕ) :
⇑zmod.χ₈ ↑n = ⇑zmod.χ₈ ↑(n % 8)

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

source
theorem zmod.χ₈_int_mod_eight (n : ℤ) :
⇑zmod.χ₈ ↑n = ⇑zmod.χ₈ ↑(n % 8)

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

source
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

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

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

Equations
source
theorem zmod.is_quadratic_χ₈'  :
zmod.χ₈'.is_quadratic

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

source
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

source
theorem zmod.χ₈'_nat_eq_if_mod_eight (n : ℕ) :
⇑zmod.χ₈' ↑n = ite (n % 2 = 0) 0 (ite (n % 8 = 1 ∨ n % 8 = 3) 1 (-1))
source
theorem zmod.χ₈'_eq_χ₄_mul_χ₈ (a : zmod 8) :
⇑zmod.χ₈' a = ⇑zmod.χ₄ ↑a * ⇑zmod.χ₈ a

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

source
theorem zmod.χ₈'_int_eq_χ₄_mul_χ₈ (a : ℤ) :
⇑zmod.χ₈' ↑a = ⇑zmod.χ₄ ↑a * ⇑zmod.χ₈ ↑a