# 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`.

source
def ZMod.χ₄ :
MulChar (ZMod 4) ℤ

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

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

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

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

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

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

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

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

An explicit description of `χ₄` on integers / naturals

source
theorem ZMod.χ₄_nat_eq_if_mod_four (n : ℕ) :
χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
source
theorem ZMod.χ₄_eq_neg_one_pow {n : ℕ} (hn : n % 2 = 1) :
χ₄ ↑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) :
χ₄ ↑n = 1

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

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

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

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

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

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

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

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

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

source
def ZMod.χ₈ :
MulChar (ZMod 8) ℤ

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

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

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

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

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

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

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

source
theorem ZMod.χ₈_int_eq_if_mod_eight (n : ℤ) :
χ₈ ↑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

source
theorem ZMod.χ₈_nat_eq_if_mod_eight (n : ℕ) :
χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
source
def ZMod.χ₈' :
MulChar (ZMod 8) ℤ

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

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

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

source
theorem ZMod.χ₈'_int_eq_if_mod_eight (n : ℤ) :
χ₈' ↑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

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

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

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