quadraticChar_isQuadratic
theorem quadraticChar_isQuadratic :
∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], (quadraticChar F).IsQuadratic := by
sorry
The theorem `quadraticChar_isQuadratic` states that for any type `F` which has a field structure, finite type structure, and a decidable equality, the quadratic character of `F` is indeed a quadratic multiplicative character. This means that for any element of `F`, the quadratic character of that element will always take the values `0`, `1`, or `-1`.
More concisely: For any field `F` with a decidable equality, the quadratic character map on `F` is a multiplicative character taking values in {0, 1, -1}.
|
Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic._auxLemma.4
theorem Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic._auxLemma.4 :
∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], (1 = 0) = False
This theorem, part of the Mathlib library in Number Theory, specifically under Legendre Symbol and Quadratic Characters, asserts that for any type `α` that has zero and one as instances and for which one is not zero (`NeZero`), the equality `1 = 0` is always false. In other words, in any number system where "one" and "zero" are defined and "one" is not equal to "zero", one cannot be equal to zero. This is a fundamental concept in most number systems in mathematics.
More concisely: In any type with defined zero and one where one is non-zero, the equality of one and zero always holds false.
|
quadraticChar_isNontrivial
theorem quadraticChar_isNontrivial :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → (quadraticChar F).IsNontrivial
This theorem states that for any field `F`, which has a finite number of elements and a decidable equality operation, if the characteristic of `F` is not 2 (in other words, if the characteristic is odd), then the quadratic character of `F` is nontrivial as a multiplicative character. The characteristic of a field is the smallest positive integer `n` such that `n * 1 = 0` in the field, and a quadratic character is a function that maps elements of the field to integers and satisfies certain properties under multiplication. A nontrivial character is one that is not identically equal to 1. Therefore, this theorem is asserting a relationship between the characteristic of a field and the nontriviality of its quadratic character.
More concisely: For any finite odd-characteristic field F, its quadratic character is a nontrivial multiplicative character.
|
quadraticCharFun_eq_one_of_char_two
theorem quadraticCharFun_eq_one_of_char_two :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F = 2 → ∀ {a : F}, a ≠ 0 → quadraticCharFun F a = 1
The theorem `quadraticCharFun_eq_one_of_char_two` states that for any field `F` which has a finite number of elements and a decidable equality, if the characteristic of the field `F` is `2`, then the quadratic character function `quadraticCharFun` evaluates to `1` on all nonzero elements of the field. Essentially, this theorem relates the characteristic of a field with the behavior of the quadratic character function on that field, specifying that the quadratic character function returns `1` for all nonzero elements when the field has characteristic `2`.
More concisely: If `F` is a finite field with decidable equality and characteristic 2, then the quadratic character function `quadraticCharFun` evaluates to 1 for all nonzero elements in `F`.
|
Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic._auxLemma.7
theorem Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic._auxLemma.7 :
∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], ((if P then a else b) = a) = (¬P → b = a)
This theorem, labeled as `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic._auxLemma.7`, states that for any sort `α` and any elements `a` and `b` of `α`, along with a proposition `P` for which we can decide whether it is true or false, the equality of the result of a conditional statement `if P then a else b` to `a` is equivalent to the assertion that if `P` is not true, then `b` equals `a`. In other words, if `P` is false, then `b` must be `a` for the conditional statement to still result in `a`.
More concisely: The theorem `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic._auxLemma.7` in Lean 4 states that the equality of `a` and `if P then a else b` holds if and only if `b = a` whenever `P` is false.
|
quadraticChar_sum_zero
theorem quadraticChar_sum_zero :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → (Finset.univ.sum fun a => (quadraticChar F) a) = 0
This theorem, named `quadraticChar_sum_zero`, states that for all fields `F` which are finite and have decidable equality, if the characteristic of the field `F` is not equal to 2 (i.e., it is odd), then the sum of the values of the quadratic character over all elements of the field (i.e., over the universal finite set) is equal to zero. The quadratic character is a function mapping elements of the field to integers, and this theorem asserts a certain property of this function when summed over the whole field under a specific condition on the characteristic of the field.
More concisely: For a finite field F with decidable equality and odd characteristic, the sum of values of its quadratic character over all elements is zero.
|
quadraticCharFun_zero
theorem quadraticCharFun_zero :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], quadraticCharFun F 0 = 0 := by
sorry
This theorem, `quadraticCharFun_zero`, states that for any field `F` of a given type `u_1`, if `F` is finite (`Fintype`) and has decidable equality (`DecidableEq`), then the quadratic character function (`quadraticCharFun`) of `F` evaluated at zero (`0`) equals to zero. Here, a field is a set on which addition, subtraction, multiplication, and division are defined, and satisfy certain mathematical laws. `Fintype` means that the field is finite, and `DecidableEq` indicates that we can decide whether any two elements in the field are equal or not. The quadratic character function is a type of function in mathematics often encountered in number theory and algebra.
More concisely: If `F` is a finite field of type `u_1` with decidable equality, then `quadraticCharFun F 0` equals to `0`.
|
quadraticChar_neg_one
theorem quadraticChar_neg_one :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → (quadraticChar F) (-1) = ZMod.χ₄ ↑(Fintype.card F)
This theorem states that for a given field `F` that has a decidable equality and is a finite type, if the unique characteristic of the semiring `F` is not 2, then the value of the quadratic character at `-1` in `F` is equal to the value of the nontrivial quadratic character on `ZMod 4` evaluated at the number of elements in `F`. The theorem essentially provides a connection between the quadratic character of a field and its number of elements under certain conditions.
More concisely: If `F` is a finite field with decidable equality and characteristic different from 2, then the quadratic character of `-1` in `F` equals the nontrivial quadratic character on `ZMod 4` evaluated at the number of elements in `F`.
|
quadraticChar_sq_one
theorem quadraticChar_sq_one :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
a ≠ 0 → (quadraticChar F) a ^ 2 = 1
This theorem states that for any field `F` that has a finite number of elements and decidable equality, the square of the quadratic character on any nonzero element `a` of `F` is `1`. In other words, if `a` is a nonzero element of a finite field `F`, then squaring the quadratic character of `a` yields `1`.
More concisely: For any finite field `F` with decidable equality, the quadratic character of any nonzero element `a` in `F` satisfies ` quadratic_char (a) ^ 2 = 1`.
|
quadraticChar_sq_one'
theorem quadraticChar_sq_one' :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
a ≠ 0 → (quadraticChar F) (a ^ 2) = 1
The theorem `quadraticChar_sq_one'` asserts that for any field `F` with decidable equality and finite type, if `a` is a nonzero element of `F`, the quadratic character of `F` evaluated at the square of `a` equals `1`. In other words, in the context of a given field, the quadratic character function assigns the value `1` to the square of any nonzero element.
More concisely: For any field with decidable equality and finite type, the quadratic character equals 1 when evaluated at the square of any nonzero element.
|
quadraticChar_eq_pow_of_char_ne_two
theorem quadraticChar_eq_pow_of_char_ne_two :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → (quadraticChar F) a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
This theorem states that for any finite field `F` with decidable equality, if the characteristic of the ring `F` is not equal to 2, then for any nonzero element `a` of `F`, the quadratic character of `a` in `F` can be determined by the parity of `a` raised to the power of the number of elements in `F` divided by 2. Specifically, if `a` raised to the power of half the size of the field equals 1, the quadratic character is 1, otherwise, it is -1.
More concisely: For a finite field `F` with decidable equality and characteristic different from 2, the quadratic character of a nonzero element `a` is equal to (1 ^ (#F / 2))^2, where #F denotes the number of elements in `F`.
|
quadraticChar_dichotomy
theorem quadraticChar_dichotomy :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
a ≠ 0 → (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1
This theorem states that for any field `F` with a finite number of elements and a decidable equality, the quadratic character of any non-zero element `a` from `F` is either `1` or `-1`. In mathematical terms, given a field `F` that is finite and for which equality is decidable, if `a` is any non-zero element in `F`, then the quadratic character of `a` is either `1` or `-1`.
More concisely: In a finite field `F` with decidable equality, the quadratic character of any non-zero element `a` is either 1 or -1.
|
quadraticChar_eq_zero_iff
theorem quadraticChar_eq_zero_iff :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
(quadraticChar F) a = 0 ↔ a = 0
This theorem states that for any field `F`, which has finitely many elements and a decidable equality, the value of the quadratic character on any element `a` of `F` is zero if and only if `a` is zero. In other words, the quadratic character function maps `a` to zero precisely when `a` is zero in the field.
More concisely: For any finite decidable field F, the quadratic character function equals zero if and only if the argument is the additive identity of F.
|
quadraticCharFun_mul
theorem quadraticCharFun_mul :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] (a b : F),
quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
This theorem, named "quadraticCharFun_mul", states that the quadratic character function is multiplicative over a field `F`. Specifically, for all elements `a` and `b` of the field `F`, the quadratic character of their product, `a * b`, is equal to the product of the quadratic character of `a` and the quadratic character of `b`. Here, `F` is a field, that is, a set with two operations (addition and multiplication) satisfying certain properties, and the field `F` is assumed to be a finite type, meaning it has a finite number of elements. Also, it is assumed that the equality between elements of `F` is decidable, meaning for any two elements `a` and `b` in `F`, it is possible to decide whether `a` is equal to `b`.
More concisely: For all elements a and b in a finite field F, the quadratic character of their product a * b is equal to the product of the quadratic characters of a and b.
|
quadraticChar_eq_neg_one_iff_not_one
theorem quadraticChar_eq_neg_one_iff_not_one :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
a ≠ 0 → ((quadraticChar F) a = -1 ↔ ¬(quadraticChar F) a = 1)
This theorem states that for any field `F` that has a finite number of elements and decidable equality, and for any non-zero element `a` of `F`, the quadratic character of `F` evaluated at `a` equals `-1` if and only if it does not equal `1`. In other words, the value of the quadratic character on non-zero elements of the field is either `1` or `-1`.
More concisely: For any finite field with decidable equality, the quadratic character takes the value -1 on non-zero elements if and only if it is not equal to 1.
|
quadraticChar_exists_neg_one
theorem quadraticChar_exists_neg_one :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → ∃ a, (quadraticChar F) a = -1
The theorem `quadraticChar_exists_neg_one` states that for any field `F` (which also has a finite number of elements and decidable equality), if the unique characteristic of the field `F` is not 2 (i.e., `F` has odd characteristic), then there exists an element `a` in `F` such that applying the quadratic character function `quadraticChar` to `a` yields `-1`. This suggests that in a field with odd characteristic, the quadratic character function can take negative values.
More concisely: In a finite odd characteristic field, the quadratic character function assumes the value -1 for some element.
|
FiniteField.isSquare_neg_one_iff
theorem FiniteField.isSquare_neg_one_iff :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F], IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
The theorem `FiniteField.isSquare_neg_one_iff` states that for any finite field `F`, `-1` is a square in `F` if and only if the cardinality (number of elements) of `F` is not congruent to `3` modulo `4`. In other words, `-1` can be represented as the square of some element in `F` precisely when the number of elements in `F` leaves a remainder other than `3` when divided by `4`.
More concisely: In a finite field, the negative of the identity element is a square if and only if the field has an even number of elements and is not isomorphic to the finite field of order 3.
|
quadraticChar_eq_one_of_char_two
theorem quadraticChar_eq_one_of_char_two :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F = 2 → ∀ {a : F}, a ≠ 0 → (quadraticChar F) a = 1
This theorem states that for any field `F` of finite type with decidable equality, if the unique characteristic of the semiring structure of `F` is `2`, then the quadratic character of `F` evaluates to `1` for all nonzero elements of `F`. In other words, if the ring characteristic of a field is `2`, then all nonzero elements of the field are mapped to `1` by the quadratic character.
More concisely: For any field of finite type with decidable equality and characteristic 2, the quadratic character maps all nonzero elements to 1.
|
quadraticChar_neg_one_iff_not_isSquare
theorem quadraticChar_neg_one_iff_not_isSquare :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
(quadraticChar F) a = -1 ↔ ¬IsSquare a
The theorem `quadraticChar_neg_one_iff_not_isSquare` states that for a given field `F` with a finite number of elements and decidable equality, for any element `a` of `F`, the quadratic character of `F` at `a` is equal to `-1` if and only if `a` is not a square in `F`. In other words, an element `a` of the field `F` is not expressible as the square of some other element of `F` if and only if the quadratic character function evaluates to `-1` at `a`.
More concisely: For a finite field F with decidable equality, an element a of F is not a square if and only if the quadratic character of F at a equals -1.
|
quadraticChar_card_sqrts
theorem quadraticChar_card_sqrts :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → ∀ (a : F), ↑{x | x ^ 2 = a}.toFinset.card = (quadraticChar F) a + 1
This theorem states that for any field `F` which is finite and has decidable equality, and whose ring characteristic is not 2, the number of solutions to the equation `x^2 = a` for any element `a` in `F`, is determined by the quadratic character of `F`. Specifically, the cardinality of the set of solutions is equal to the evaluation of the quadratic character at `a` plus 1. The quadratic character in this context is a certain function associated with the field `F`, constructed as a multiplicative character.
More concisely: For a finite field `F` with decidable equality and characteristic not equal to 2, the number of solutions to the quadratic equation `x^2 = a` in `F` equals the quadratic character of `a` in `F` plus 1.
|
quadraticCharFun_eq_zero_iff
theorem quadraticCharFun_eq_zero_iff :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
quadraticCharFun F a = 0 ↔ a = 0
The theorem `quadraticCharFun_eq_zero_iff` states that for any field `F`, which also has finite type and decidable equality, and any element `a` of `F`, the quadratic characteristic function of `F` evaluated at `a` is zero if and only if `a` is zero. This theorem provides a necessary and sufficient condition for the quadratic characteristic function of a field to be zero at a particular point in terms of the value of that point being zero.
More concisely: For any field F of finite type with decidable equality, the quadratic characteristic function of F equals zero at an element a if and only if a is zero.
|
quadraticChar_one_iff_isSquare
theorem quadraticChar_one_iff_isSquare :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F},
a ≠ 0 → ((quadraticChar F) a = 1 ↔ IsSquare a)
The theorem `quadraticChar_one_iff_isSquare` states that for any given nonzero element `a` of any field `F`, the quadratic character of `F` evaluated at `a` equals `1` if and only if `a` is a square in the field `F`. In other words, if `a` in field `F` is not zero, then the function `quadraticChar F` returns `1` when applied to `a` if and only if there exists some `r` in field `F` such that `a = r * r`.
More concisely: For any nonzero element `a` in a field `F`, the quadratic character of `F` evaluated at `a` equals 1 if and only if `a` is a square in `F`. (Equivalently, `a` is a root of some `x^2` in `F[x]`.)
|
quadraticCharFun_eq_pow_of_char_ne_two
theorem quadraticCharFun_eq_pow_of_char_ne_two :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
This theorem states that for any field `F` that has a finite number of elements and a decidable equality, if the unique characteristic of the field `F` is not equal to 2, then for any non-zero element `a` of `F`, the quadratic character function of `F` with `a` can be computed as follows: if `a` to the power of half the number of elements in `F` equals 1, then the quadratic character function equals 1, otherwise it equals -1.
More concisely: If `F` is a finite field with a decidable equality and characteristic different from 2, then the quadratic character function of a non-zero element `a` in `F` is equal to 1 if `a` raised to the power of half the number of elements in `F` is equal to 1, and equal to -1 otherwise.
|