quadraticChar_card_card
theorem quadraticChar_card_card :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 →
∀ {F' : Type u_2} [inst_3 : Field F'] [inst_4 : Fintype F'] [inst_5 : DecidableEq F'],
ringChar F' ≠ 2 →
ringChar F' ≠ ringChar F →
(quadraticChar F) ↑(Fintype.card F') =
(quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
This theorem establishes a relationship between the quadratic characters of two different fields, `F` and `F'`, based on their cardinalities. The cardinality is the number of elements in each field. Specifically, if the unique characteristic of the semiring of fields `F` and `F'` is not equal to 2, and these characteristics are not equal to each other, then the value of the quadratic character of `F` at the cardinality of `F'` is equal to the value of the quadratic character of `F'` at the product of the value of the quadratic character of `F` at `-1` and the cardinality of `F`. The quadratic character is a multiplicative character, meaning it's a function with certain multiplicative properties. The concept of decidability is also involved, which means we can determine whether two elements of a field are equal.
More concisely: If char F ≠ char F' ≠ 2, then quadratic_character F (cardinality F') = quadratic_character F (-1) ^ cardinality F' where quadratic_character is a multiplicative character on the semiring of fields.
|
quadraticChar_two
theorem quadraticChar_two :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → (quadraticChar F) 2 = ZMod.χ₈ ↑(Fintype.card F)
This theorem, `quadraticChar_two`, states that for any field `F` that has a finite number of elements and a decidable equality, if the unique characteristic of this field (denoted by `ringChar F`) is not equal to `2`, then the value of the quadratic character at `2` for this field is equal to `ZMod.χ₈` evaluated at the cardinality (the number of elements) of the field. That is, the quadratic character of a field at `2` corresponds to a specific primitive quadratic character on `ZMod 8`, as long as the ring characteristic of the field is not `2`.
More concisely: For a finite field F with decidable equality and characteristic not equal to 2, the quadratic character at 2 is equal to the primitive quadratic character ZMod.χ⁶ on the field's cardinality.
|
FiniteField.isSquare_two_iff
theorem FiniteField.isSquare_two_iff :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F],
IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5
The theorem `FiniteField.isSquare_two_iff` states that for any finite field `F`, the number `2` is a perfect square in this field if and only if the cardinality of the field, i.e., the number of elements in the field, modulo `8` is neither `3` nor `5`. In other words, `2` can be expressed as the square of some element in the field `F` exactly when the number of elements in `F`, when divided by `8`, does not leave a remainder of `3` or `5`.
More concisely: In a finite field, the element 2 is a perfect square if and only if the field's cardinality is congruent to 1 or 6 modulo 8.
|
quadraticChar_neg_two
theorem quadraticChar_neg_two :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 → (quadraticChar F) (-2) = ZMod.χ₈' ↑(Fintype.card F)
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 semiring (ringChar) of `F` is not equal to 2, then the value of the quadratic character of `F` at `-2` is equal to the second primitive quadratic character on `ZMod 8`, evaluated at the cardinality (number of elements) of the field `F`. It implies a connection between the quadratic property of a field and its cardinality under specific conditions.
More concisely: If `F` is a finite field with a decidable equality and ring characteristic different from 2, then the quadratic character of `F` at `-2` equals the second primitive quadratic character of `ZMod 8` evaluated at the cardinality of `F`.
|
FiniteField.isSquare_neg_two_iff
theorem FiniteField.isSquare_neg_two_iff :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F],
IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7
This theorem states that for any finite field `F`, the number `-2` is a square in `F` if and only if the cardinality of `F` (denoted by `#F`), when divided by 8, does not leave a remainder of 5 or 7. Here, a number `a` is considered a square in `F` if there exists another number `r` in `F` such that `a = r * r`.
More concisely: For a finite field `F`, the number `-2` is a square if and only if the cardinality `#F` is congruent to 0, 1, 4 or 6 modulo 8.
|
quadraticChar_odd_prime
theorem quadraticChar_odd_prime :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
ringChar F ≠ 2 →
∀ {p : ℕ} [inst_3 : Fact p.Prime],
p ≠ 2 →
ringChar F ≠ p →
(quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))
The theorem `quadraticChar_odd_prime` states that for any field `F` that has a finite number of elements and decidable equality, with a ring characteristic not equal to 2, and for any odd prime number `p` not equal to 2 and the ring characteristic of `F`, the value of the quadratic character of `F` at `p` is equal to the value of the quadratic character of the integers modulo `p` at the product of the character `χ₄` of the set `ZMod` evaluated at the size of `F` and the size of `F`. Essentially, this theorem links the quadratic character of a field at an odd prime number to the quadratic character on a ring of integers modulo that prime, under certain assumptions.
More concisely: For a finite field F with decidable equality and characteristic not equal to 2, the quadratic character of F at an odd prime p not equals 2 is equal to the product of the quadratic character of the integers modulo p at p and the size of F.
|
FiniteField.isSquare_odd_prime_iff
theorem FiniteField.isSquare_odd_prime_iff :
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F],
ringChar F ≠ 2 →
∀ {p : ℕ} [inst_2 : Fact p.Prime],
p ≠ 2 → (IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1)
The theorem `FiniteField.isSquare_odd_prime_iff` states that for any finite field `F` of characteristic not equal to 2, an odd prime number `p` is a square in `F` if and only if the quadratic character of the integers modulo `p` does not take the value `-1` on the product of `χ₄` of `F` (which corresponds to the extension `ℚ(√-1)/ℚ`) and the cardinality of `F`. Here, the quadratic character of a field is a kind of function that captures information about quadratic residues, and being a "square" in `F` means that `p` can be expressed as the square of some element of `F`.
More concisely: For a finite field F of characteristic not 2, an odd prime number p is a square in F if and only if the quadratic character of F evaluates to neither 1 nor -1 on χ₄ of F and the cardinality of F.
|