gaussSum_frob
theorem gaussSum_frob :
∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
[fp : Fact p.Prime] [hch : CharP R' p] (χ : MulChar R R') (ψ : AddChar R R'),
gaussSum χ ψ ^ p = gaussSum (χ ^ p) (ψ ^ p)
This theorem states that for any two types `R` and `R'`, where `R` forms a finite commutative ring and `R'` forms a commutative ring with prime characteristic `p`, the `p`th power of the Gauss sum associated to a multiplicative character `χ` and an additive character `ψ` equals the Gauss sum associated to the `p`th power of `χ` and the `p`th power of `ψ`. In other words, raising the Gauss sum of `χ` and `ψ` to the power `p` yields the same result as taking the Gauss sum of `χ^p` and `ψ^p`. This property holds when `p` is a prime number. The Gauss sum is a summation over all elements of the ring `R`, with each term being the product of the multiplicative character value and the additive character value for that element.
More concisely: For any finite commutative rings R and commutative rings R' of prime characteristic p, the p-th power of the Gauss sum of a multiplicative character χ and an additive character ψ equals the Gauss sum of χ^p and ψ^p.
|
gaussSum_sq
theorem gaussSum_sq :
∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [inst_3 : IsDomain R']
{χ : MulChar R R'},
χ.IsNontrivial →
χ.IsQuadratic → ∀ {ψ : AddChar R R'}, ψ.IsPrimitive → gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
The theorem `gaussSum_sq` states that for any field 'R' with a finite number of elements and any commutative ring 'R'', given a multiplicative character 'χ' of 'R' into 'R'' that is nontrivial and quadratic, and a primitive additive character 'ψ' of 'R' into 'R'', the square of the Gauss sum of 'χ' and 'ψ' equals the value of 'χ' at -1 multiplied by the cardinality (i.e., number of elements) of 'R'. Essentially, this theorem provides a specific value for the square of the Gauss sum under these conditions, linking it to the properties of the multiplicative character and the size of the field.
More concisely: For any finite field 'R' with a multiplicative character 'χ' that is nontrivial and quadratic, and a primitive additive character 'ψ' of 'R', the square of the Gauss sum of 'χ' and 'ψ' equals the cardinality of 'R' times 'χ'(-1).
|
FiniteField.two_pow_card
theorem FiniteField.two_pow_card :
∀ {F : Type u_1} [inst : Fintype F] [inst_1 : Field F],
ringChar F ≠ 2 → 2 ^ (Fintype.card F / 2) = ↑(ZMod.χ₈ ↑(Fintype.card F))
This theorem asserts that for any finite field `F` with an odd characteristic (meaning that the unique characteristic of the semiring is not `2`), the number `2` raised to the power of the number of elements in the field divided by `2` is equal to the value of the first primitive quadratic character on `ZMod 8`, denoted as `χ₈`, evaluated at the number of elements in the field. In mathematical notation, this can be expressed as: if `F` is a finite field with `#F` elements and `char(F)` is not `2`, then `2^(#F/2) = χ₈(#F)`.
More concisely: For a finite field `F` with odd characteristic, the value of the first primitive quadratic character `χ₈` on the number of elements in `F` equals `2^(#F/2)`.
|
MulChar.IsQuadratic.gaussSum_frob
theorem MulChar.IsQuadratic.gaussSum_frob :
∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
[fp : Fact p.Prime] [hch : CharP R' p],
IsUnit ↑p → ∀ {χ : MulChar R R'}, χ.IsQuadratic → ∀ (ψ : AddChar R R'), gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ
The theorem `MulChar.IsQuadratic.gaussSum_frob` states that for any finite commutative ring `R`, its target ring `R'`, and a prime number `p` that is a unit in the ring `R`, if we have a quadratic multiplicative character `χ` and an additive character `ψ`, then the `p`th power of the Gauss sum of `χ` and `ψ` equals `χ p` times the original Gauss sum. The Gauss sum is defined as the sum over all elements `a` in `R` of the product of `χ a` and `ψ a`. The quadratic character `χ` is a homomorphism from `R` to `R'` that preserves multiplication and squares to the trivial character.
More concisely: For any finite commutative ring R, prime unit p in R, quadratic multiplicative character χ, and additive character ψ, the p-th power of the Gauss sum of χ and ψ equals χ(p) times the original Gauss sum.
|
MulChar.IsQuadratic.gaussSum_frob_iter
theorem MulChar.IsQuadratic.gaussSum_frob_iter :
∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
[fp : Fact p.Prime] [hch : CharP R' p] (n : ℕ),
IsUnit ↑p →
∀ {χ : MulChar R R'}, χ.IsQuadratic → ∀ (ψ : AddChar R R'), gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
This theorem states that for any quadratic multiplicative character `χ`, commutative rings `R` and `R'`, and additive character `ψ`, if the characteristic `p` of the target ring `R'` is a unit in the source ring `R` and `p` is prime, then the `p^n`-th power of the Gauss sum of `χ` and `ψ` is equal to `χ` evaluated at `p^n` times the original Gauss sum, where `n` is a natural number. In other words, raising the Gauss sum of `χ` and `ψ` to the power of `p^n` results in a Gaussian sum multiplied by the evaluation of the quadratic character `χ` at `p^n`.
More concisely: For any quadratic character `χ`, additive character `ψ`, natural number `n`, commutative rings `R` and `R'` with `p` as a unit in `R`, where `p` is prime, the `p^n`-th power of the Gauss sum of `χ` and `ψ` in `R'` equals `χ(p^n) *` the original Gauss sum of `χ` and `ψ` in `R`.
|
gaussSum_mul_gaussSum_eq_card
theorem gaussSum_mul_gaussSum_eq_card :
∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [inst_3 : IsDomain R']
{χ : MulChar R R'},
χ.IsNontrivial → ∀ {ψ : AddChar R R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)
The theorem `gaussSum_mul_gaussSum_eq_card` proves a property about the Gauss sum in the context of number theory, particularly in relation to a finite field `R`. The theorem asserts that if we have a multiplicative character `χ` which is nontrivial, and an additive character `ψ` which is primitive, then the product of the Gauss sum of `χ` and `ψ` and the Gauss sum of the inverse of `χ` and `ψ` is equal to the cardinality of the field `R`. In simpler terms, this theorem demonstrates a relationship between Gauss sums and the number of elements in the field that these characters are defined over.
More concisely: For a finite field `R` with a nontrivial multiplicative character `χ` and a primitive additive character `ψ`, the product of the Gauss sums of `χ` and `ψ`, and the inverse of `χ` and `ψ`, equals the cardinality of `R`.
|
gaussSum_mulShift
theorem gaussSum_mulShift :
∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ : MulChar R R')
(ψ : AddChar R R') (a : Rˣ), χ ↑a * gaussSum χ (ψ.mulShift ↑a) = gaussSum χ ψ
This theorem states that, for any commutative ring `R`, another commutative ring `R'`, a multiplicative character `χ` from `R` to `R'`, an additive character `ψ` from `R` to `R'`, and a nonzero element `a` of `R`, replacing the additive character `ψ` in the Gauss sum by `ψ.mulShift ↑a` (which shifts `ψ` by `a`) and multiplying the Gauss sum by `χ a` leaves the Gauss sum unchanged. In other words, the Gauss sum exhibits a certain kind of symmetry under the operation of shifting the additive character and scaling the multiplicative character.
More concisely: For any commutative rings `R` and `R'`, multiplicative character `χ` from `R` to `R'`, additive character `ψ` from `R` to `R'`, and nonzero element `a` in `R`, the Gauss sum is invariant under the transformation `χ a ⊤ (ψ.mulShift ↑a)`, where `⊤` denotes the transpose operation.
|