ZMod.χ₄_nat_mod_four
theorem ZMod.χ₄_nat_mod_four : ∀ (n : ℕ), ZMod.χ₄ ↑n = ZMod.χ₄ ↑(n % 4)
The theorem `ZMod.χ₄_nat_mod_four` states that for any natural number `n`, the value of `χ₄ n` is only dependent on the remainder of `n` when divided by 4. In other words, the quadratic character `χ₄` on `ZMod 4` mapped to any natural number `n` is the same as it mapped to the remainder of `n` divided by 4. This theorem links the quadratic character to the concept of congruence in modular arithmetic.
More concisely: For all natural numbers n, the quadratic character χ₄ on ZMod 4 maps n to the same value as the remainder of n divided by 4.
|
ZMod.χ₄_eq_neg_one_pow
theorem ZMod.χ₄_eq_neg_one_pow : ∀ {n : ℕ}, n % 2 = 1 → ZMod.χ₄ ↑n = (-1) ^ (n / 2)
This theorem presents an alternative characterization for the nontrivial quadratic character `χ₄` on the integers modulo 4, when applied to an odd natural number `n`. It states that for any natural number `n` such that `n mod 2 = 1` (which ensures `n` is odd), the result of applying `χ₄` to `n` (converted into an integer modulo 4) is equivalent to `-1` raised to the power of `n divided by 2`.
In other words, for odd natural numbers, the quadratic character `χ₄` can be computed as the power of `-1` where the exponent is the integer division of `n` by 2.
More concisely: For odd natural numbers n, the quadratic character χ₄ maps n to (-1)^(n/2) modulo 4.
|
ZMod.χ₄_int_mod_four
theorem ZMod.χ₄_int_mod_four : ∀ (n : ℤ), ZMod.χ₄ ↑n = ZMod.χ₄ ↑(n % 4)
The theorem `ZMod.χ₄_int_mod_four` states that for any integer `n`, the value of `χ₄ n` is only dependent on the remainder of `n` when divided by 4 (i.e., `n mod 4`). In other words, `χ₄ n` is periodic with a period of 4 in the integers. This corresponds to the mathematical statement that the nontrivial quadratic character on `ZMod 4`, denoted `χ₄`, is a function from the integers to the integers that respects congruence modulo 4.
More concisely: The theorem `ZMod.χ₄_int_mod_four` asserts that the nontrivial quadratic character `χ₄` on `ZMod 4` is a function of the integer congruence class modulo 4.
|
ZMod.χ₈_int_mod_eight
theorem ZMod.χ₈_int_mod_eight : ∀ (n : ℤ), ZMod.χ₈ ↑n = ZMod.χ₈ ↑(n % 8)
The theorem `ZMod.χ₈_int_mod_eight` states that for any integer `n`, the value of the first primitive quadratic character on `ZMod 8`, denoted as `χ₈`, at `n` is the same as its value at the remainder of `n` divided by `8`. This implies that the behavior of `χ₈` is periodic with period `8` in the integers.
More concisely: For any integer `n`, the first primitive quadratic character `χ₈` on `ZMod 8` equals its value at the remainder of `n` modulo `8`.
|
ZMod.χ₄_nat_three_mod_four
theorem ZMod.χ₄_nat_three_mod_four : ∀ {n : ℕ}, n % 4 = 3 → ZMod.χ₄ ↑n = -1
This theorem states that for any natural number `n`, if `n` modulo 4 equals 3, then the nontrivial quadratic character `χ₄` (corresponding to the extension `ℚ(√-1)/ℚ`) of `n` (when `n` is considered as an element of the ring of integers modulo 4) is equal to -1.
More concisely: For any natural number `n`, if `n` is congruent to 3 modulo 4, then the quadratic character `χ₄` of `n` equals -1.
|
ZMod.χ₄_int_three_mod_four
theorem ZMod.χ₄_int_three_mod_four : ∀ {n : ℤ}, n % 4 = 3 → ZMod.χ₄ ↑n = -1
This theorem states that for any integer `n`, if `n` modulo 4 equals 3, then applying the nontrivial quadratic character `χ₄` (which corresponds to the extension `ℚ(√-1)/ℚ`) to `n` yields -1. This character, defined on `ZMod 4`, maps each integer `n` modulo 4 to either 0, 1, or -1, and this theorem specifically deals with the case where `n modulo 4` is 3.
More concisely: For any integer `n`, if `n` is congruent to 3 modulo 4, then the nontrivial quadratic character `χ₄` maps `n` to -1.
|
ZMod.χ₄_nat_one_mod_four
theorem ZMod.χ₄_nat_one_mod_four : ∀ {n : ℕ}, n % 4 = 1 → ZMod.χ₄ ↑n = 1
This theorem states that for any natural number 'n', if 'n' modulo 4 equals 1, then the nontrivial quadratic character on `ZMod 4`, denoted as `χ₄`, evaluated at 'n' is equal to 1. The nontrivial quadratic character `χ₄` is defined within the context of modular arithmetic and specifically corresponds to the extension `ℚ(√-1)/ℚ`.
More concisely: For any natural number n, if n is congruent to 1 modulo 4, then the value of the nontrivial quadratic character χ₄ on ZMod 4 at n is equal to 1.
|
ZMod.isQuadratic_χ₈
theorem ZMod.isQuadratic_χ₈ : ZMod.χ₈.IsQuadratic
The theorem `ZMod.isQuadratic_χ₈` states that the first primitive quadratic character on `ZMod 8`, denoted as `χ₈`, takes values in the set `{0, 1, -1}`. In other words, the function `χ₈` defined on the integers modulo 8 maps each input to either 0, 1, or -1. The quadratic character `χ₈` corresponds to the extension `ℚ(√2)/ℚ` in number theory.
More concisely: The first primitive quadratic character `χ₈` on `ZMod 8` maps each integer to an element in the set {0, 1, -1}.
|
ZMod.isQuadratic_χ₄
theorem ZMod.isQuadratic_χ₄ : ZMod.χ₄.IsQuadratic
The theorem `ZMod.isQuadratic_χ₄` states that the nontrivial quadratic character `χ₄` on the integers modulo 4, which corresponds to the extension `ℚ(√-1)/ℚ`, takes its values in the set `{0, 1, -1}`. In other words, the function `χ₄` maps any integer modulo 4 to either 0, 1, or -1. This is a property of the character `χ₄`, showing its specific behavior in the context of quadratic number theory.
More concisely: The quadratic character `χ₄` on integers modulo 4 takes values in the set {0, 1, -1}.
|
ZMod.χ₈'_int_eq_if_mod_eight
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
This theorem provides an explicit description of the function `χ₈'` when applied to integers. Specifically, for any integer `n`, the value of `χ₈'` at `n` is determined by the remainder of `n` when divided by 2 and 8. If `n` is even (i.e., `n` modulo 2 is 0), then `χ₈'` at `n` is 0. If `n` is odd, then we look at `n` modulo 8. If the remainder is either 1 or 3, then `χ₈'` at `n` is 1; otherwise, it is -1. This function `χ₈'` is a second primitive quadratic character on `ZMod 8`, corresponding to the extension `ℚ(√-2)/ℚ`.
More concisely: The second primitive quadratic character χ′ on integers modulo 8 is given by χ′(n) = (if n is even then 0 else if n mod 8 is 1 or 3 then 1 else -1).
|
ZMod.χ₈'_eq_χ₄_mul_χ₈
theorem ZMod.χ₈'_eq_χ₄_mul_χ₈ : ∀ (a : ZMod 8), ZMod.χ₈' a = ZMod.χ₄ a.cast * ZMod.χ₈ a
This theorem establishes the relationship between three quadratic characters on `ZMod 8` and `ZMod 4`, denoted as `χ₈'`, `χ₄`, and `χ₈`. Specifically, for every integer modulo 8 (`a : ZMod 8`), the second primitive quadratic character on `ZMod 8` (`χ₈'`) is equal to the product of the nontrivial quadratic character on `ZMod 4` (`χ₄`) and the first primitive quadratic character on `ZMod 8` (`χ₈`). In mathematical terms, this can be written as `χ₈'(a) = χ₄(a) * χ₈(a)`. The characters correspond to specific extensions of the rational numbers: `χ₈'` corresponds to `ℚ(√-2)/ℚ`, `χ₄` corresponds to `ℚ(√-1)/ℚ`, and `χ₈` corresponds to `ℚ(√2)/ℚ`.
More concisely: The second primitive quadratic character on `ZMod 8` is the product of the nontrivial quadratic character on `ZMod 4` and the first primitive quadratic character on `ZMod 8`. In other words, `χ₈'(a) = χ₄(a) * χ₈(a)` for all integers `a` modulo 8.
|
ZMod.neg_one_pow_div_two_of_one_mod_four
theorem ZMod.neg_one_pow_div_two_of_one_mod_four : ∀ {n : ℕ}, n % 4 = 1 → (-1) ^ (n / 2) = 1
This theorem states that for any natural number `n`, if `n` modulo 4 is equal to 1, then raising `-1` to the power of `n` divided by 2 equals 1. This is a property of natural numbers related to modular arithmetic and powers of negative numbers.
More concisely: For any natural number `n`, if `n` is congruent to 1 modulo 4, then `(-1)^(n/2) = 1`.
|
ZMod.χ₈_nat_mod_eight
theorem ZMod.χ₈_nat_mod_eight : ∀ (n : ℕ), ZMod.χ₈ ↑n = ZMod.χ₈ ↑(n % 8)
The theorem `ZMod.χ₈_nat_mod_eight` states that the value of the first primitive quadratic character on `ZMod 8`, denoted `χ₈`, evaluated at any natural number `n`, is equivalent to the value of `χ₈` evaluated at the residue class of `n` modulo 8. In other words, the effect of `χ₈` on a natural number depends only on the remainder of that number when divided by 8.
More concisely: The first primitive quadratic character `χ₈` on `ZMod 8` maps natural numbers to their residue classes modulo 8 equivalently.
|
ZMod.neg_one_pow_div_two_of_three_mod_four
theorem ZMod.neg_one_pow_div_two_of_three_mod_four : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1
The theorem states that for any natural number `n`, if `n` modulo 4 equals 3, then raising `-1` to the power of `n` divided by 2 equals `-1`. In other words, for any natural number that leaves a remainder of 3 when divided by 4, if we take half of that number as the exponent of `-1`, the result will be `-1`.
More concisely: For any natural number `n`, if `n` is congruent to 3 modulo 4, then `(-1)^(n/2) = -1`.
|
ZMod.isQuadratic_χ₈'
theorem ZMod.isQuadratic_χ₈' : ZMod.χ₈'.IsQuadratic
This theorem asserts that the second primitive quadratic character on `ZMod 8`, denoted as `χ₈'`, only takes values in the set `{0, 1, -1}`. In other words, for any input, the function `χ₈'` always outputs either 0, 1, or -1, with no other values possible. This character corresponds to the extension `ℚ(√-2)/ℚ` in number theory.
More concisely: The second primitive quadratic character `χ₈'` on `ZMod 8` takes values in the set {0, 1, -1}.
|
ZMod.χ₄_int_eq_if_mod_four
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 := by
sorry
This theorem provides an explicit description of the function `χ₄` on integers. For any integer `n`, the value of `χ₄` at `n` is determined according to the remainder of `n` when divided by 2 and 4. Specifically, if `n` is divisible by 2, then `χ₄` at `n` is 0. Otherwise, if `n` leaves a remainder of 1 when divided by 4, then `χ₄` at `n` is 1. In all other cases (i.e., when `n` leaves a remainder of 3 when divided by 4), `χ₄` at `n` is -1.
More concisely: The characteristic function χ₄ on integers is defined as χ₄(n) = 0 when n is even, χ₄(n) = 1 if n leaves a remainder of 1 when divided by 4, and χ₄(n) = -1 otherwise.
|
ZMod.χ₄_int_one_mod_four
theorem ZMod.χ₄_int_one_mod_four : ∀ {n : ℤ}, n % 4 = 1 → ZMod.χ₄ ↑n = 1
The theorem states that for any integer `n`, if `n` is congruent to 1 modulo 4 (i.e., if `n % 4 = 1`), then the value of the nontrivial quadratic character `χ₄` on the integers modulo 4, evaluated at `n`, equals 1. In other words, when an integer `n` leaves a remainder of 1 when divided by 4, the function `χ₄` gives us a result of 1.
More concisely: For any integer `n`, if `n` is congruent to 1 modulo 4, then the nontrivial quadratic character `χ₄` evaluated at `n` is equal to 1.
|
ZMod.χ₈_int_eq_if_mod_eight
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
This theorem provides an explicit description of the function `χ₈` acting on integers. Specifically, for any integer `n`, the value of `χ₈` at `n` is determined by the residue of `n` modulo 8. If `n` is even, then `χ₈(n)` is 0. If `n` is odd and `n` modulo 8 is either 1 or 7, then `χ₈(n)` is 1. Otherwise, if `n` is odd and `n` modulo 8 is neither 1 nor 7, then `χ₈(n)` is -1. This function `χ₈` is a primitive quadratic character on the integers modulo 8, playing a critical role in number theory, particularly in the theory of quadratic fields and modular forms.
More concisely: The theorem states that the quadratic character χ₈ on integers is given by χ₈(n) = (if n is even then 0 else if n modulo 8 is in {1, 7} then 1 else -1).
|