AddChar.to_mulShift_inj_of_isPrimitive
theorem AddChar.to_mulShift_inj_of_isPrimitive :
∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] {ψ : AddChar R R'},
ψ.IsPrimitive → Function.Injective ψ.mulShift
The theorem `AddChar.to_mulShift_inj_of_isPrimitive` states that for any commutative ring `R`, any commutative monoid `R'` and any additive character `ψ` from `R` to `R'`, if `ψ` is primitive then the function which maps each element `a` in `R` to the multiplicative shift of `ψ` by `a` is injective. In other words, if `ψ` is a primitive additive character, then no two different elements of `R` will have the same multiplicative shift under `ψ`.
More concisely: If `ψ` is a primitive additive character on a commutative ring `R`, then the function mapping each element `a` in `R` to the multiplicative shift of `ψ` by `a` is an injection.
|
AddChar.IsNontrivial.isPrimitive
theorem AddChar.IsNontrivial.isPrimitive :
∀ {R' : Type v} [inst : CommMonoid R'] {F : Type u} [inst_1 : Field F] {ψ : AddChar F R'},
ψ.IsNontrivial → ψ.IsPrimitive
This theorem states that, given any field 'F' and communicative monoid 'R', and an additive character 'ψ' from 'F' to 'R', if this additive character is nontrivial, then it is also primitive. Essentially, in the context of these mathematical structures, nontriviality of an additive character implies its primitiveness.
More concisely: If 'F' is a field and 'R' is a communicative monoid, and 'ψ' is a nontrivial additive character from 'F' to 'R', then 'ψ' is primitive.
|
AddChar.zmodChar_apply
theorem AddChar.zmodChar_apply :
∀ {C : Type v} [inst : CommMonoid C] {n : ℕ+} {ζ : C} (hζ : ζ ^ ↑n = 1) (a : ZMod ↑n),
(AddChar.zmodChar n hζ) a = ζ ^ a.val
This theorem states that for any commutative monoid `C` and a positive integer `n`, if `ζ` is an element of `C` such that `ζ` to the power of `n` equals 1, and `a` is an element of the integers modulo `n`, then the additive character on `ZMod n` defined using `ζ` sends `a` to `ζ` raised to the value of `a`. Essentially, it's stating the action of the additive character in this specific context.
More concisely: For any commutative monoid `C` with an element `ζ` of order `n`, and for any integer `a` modulo `n`, the additive character on `ZMod n` defined using `ζ` maps `a` to `ζ^a`.
|
AddChar.sum_mulShift
theorem AddChar.sum_mulShift :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : DecidableEq R] {R' : Type u_2}
[inst_3 : CommRing R'] [inst_4 : IsDomain R'] {ψ : AddChar R R'} (b : R),
ψ.IsPrimitive → (Finset.univ.sum fun x => ψ (x * b)) = ↑(if b = 0 then Fintype.card R else 0)
This theorem states that for any commutative ring `R`, with a finite number of elements and decidable equality, and another commutative ring `R'` which is also a domain, along with an additive characteristic function `ψ` from `R` to `R'` and an element `b` of `R`, if `ψ` is primitive (i.e., it satisfies certain properties), then the sum of `ψ` applied to each element of `R` multiplied by `b` is equal to the cardinality of `R` if `b` is zero, and zero otherwise. In other words, for a primitive `ψ`, the sum over all elements of `R` scaled by `b` via `ψ` equals the number of elements in `R` when `b` is zero, and zero when `b` is non-zero.
More concisely: For any commutative ring R with a finite number of elements and decidable equality, a domain R', a primitive additive characteristic function ψ from R to R', and an element b in R, the sum of b * ψ(x) over all x in R equals the cardinality of R if b is zero, and zero otherwise.
|
AddChar.zmod_char_isNontrivial_iff
theorem AddChar.zmod_char_isNontrivial_iff :
∀ {C : Type v} [inst : CommMonoid C] (n : ℕ+) (ψ : AddChar (ZMod ↑n) C), ψ.IsNontrivial ↔ ψ 1 ≠ 1
The theorem `AddChar.zmod_char_isNontrivial_iff` states that, for any positive natural number `n` and any additive character `ψ` from the integers modulo `n` (`ZMod n`) to a commutative monoid `C`, `ψ` is nontrivial if and only if the value of `ψ` at `1` is not `1`. An additive character is said to be nontrivial if there exists an element in its domain on which it doesn't return the identity of the codomain. In this case, the identity of the codomain `C` is `1`.
More concisely: An additive character from the integers modulo n to a commutative monoid is nontrivial if and only if its value at 1 is not equal to the identity of the codomain.
|
AddChar.IsPrimitive.zmod_char_eq_one_iff
theorem AddChar.IsPrimitive.zmod_char_eq_one_iff :
∀ {C : Type v} [inst : CommMonoid C] (n : ℕ+) {ψ : AddChar (ZMod ↑n) C},
ψ.IsPrimitive → ∀ (a : ZMod ↑n), ψ a = 1 ↔ a = 0
The theorem `AddChar.IsPrimitive.zmod_char_eq_one_iff` states that for any given positive integer `n`, and for any commutative monoid `C`, if `ψ` is a primitive additive character on the integers modulo `n`, then ψ takes the value `1` if and only if its input is `0`. In other words, a primitive additive character on the set of integers modulo `n` maps an integer `a` to `1` if and only if `a` is equal to `0`.
More concisely: A primitive additive character on the integers modulo n equals 1 if and only if the character's argument is 0.
|
AddChar.zmodChar_primitive_of_primitive_root
theorem AddChar.zmodChar_primitive_of_primitive_root :
∀ {C : Type v} [inst : CommMonoid C] (n : ℕ+) {ζ : C} (h : IsPrimitiveRoot ζ ↑n),
(AddChar.zmodChar n ⋯).IsPrimitive
This theorem states that for any given commutative monoid `C`, positive natural number `n`, and an element `ζ` in `C` that is a primitive `n`th root of unity, the additive character on `ZMod n` associated with `ζ` is primitive. In other words, if `ζ` is a primitive `n`th root of unity in the commutative monoid `C`, then the mapping from `ZMod n` to `C` using the power of `ζ` is a primitive character.
More concisely: If `ζ` is a primitive `n`th root of unity in a commutative monoid `C`, then the additive character on `ZMod n` defined by `x ↔=> ζ^x` is a primitive character in `C`.
|
AddChar.PrimitiveAddChar.prim
theorem AddChar.PrimitiveAddChar.prim :
∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : Field R'] (χ : AddChar.PrimitiveAddChar R R'),
χ.char.IsPrimitive
The theorem `AddChar.PrimitiveAddChar.prim` asserts that for any given types `R` and `R'`, where `R` is a commutative ring and `R'` is a field, and for any primitive additive character `χ` from `R` into a cyclotomic extension of `R'`, the character component of `χ` (denoted by `χ.char`) is necessarily primitive. This theorem essentially verifies and underlines the primitiveness of the character in the definition of `AddChar.PrimitiveAddChar`.
More concisely: If `χ` is a primitive additive character from a commutative ring `R` into a cyclotomic extension of a field `R'`, then `χ.char` is a primitive character.
|
AddChar.sum_eq_zero_of_isNontrivial
theorem AddChar.sum_eq_zero_of_isNontrivial :
∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Fintype R] {R' : Type u_2} [inst_2 : CommRing R']
[inst_3 : IsDomain R'] {ψ : AddChar R R'}, ψ.IsNontrivial → (Finset.univ.sum fun a => ψ a) = 0
This theorem states that for any type `R` which forms an additive group and is finite (has finiteness property), and any type `R'` which forms a commutative ring and is a domain, if we have an additive character `ψ : AddChar R R'` which is nontrivial (i.e., `ψ.IsNontrivial`), then the sum over the values of this additive character for all elements in `R` (represented by `Finset.univ.sum fun a => ψ a`) equals zero.
More concisely: For any finite additive group `R` and commutative ring `R'` with 1, if `ψ : R → R'` is a nontrivial additive character, then the sum of `ψ` over all elements in `R` is zero.
|
AddChar.zmod_char_primitive_of_eq_one_only_at_zero
theorem AddChar.zmod_char_primitive_of_eq_one_only_at_zero :
∀ {C : Type v} [inst : CommMonoid C] (n : ℕ) (ψ : AddChar (ZMod n) C),
(∀ (a : ZMod n), ψ a = 1 → a = 0) → ψ.IsPrimitive
This theorem states that for any commutative monoid `C` and any natural number `n`, if an additive character `ψ` mapping from the integers modulo `n` to `C` has the property that it takes the value `1` only at `0` (i.e., for every element `a` of the integers modulo `n`, ψ(a) is `1` if and only if `a` is `0`), then this additive character `ψ` is primitive. In other words, the uniqueness of the element mapping to `1` under `ψ` ensures its primitiveness.
More concisely: If an additive character from the integers modulo n to a commutative monoid maps only the zero element to 1, then it is primitive.
|
AddChar.sum_eq_card_of_is_trivial
theorem AddChar.sum_eq_card_of_is_trivial :
∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Fintype R] {R' : Type u_2} [inst_2 : CommRing R'] {ψ : AddChar R R'},
¬ψ.IsNontrivial → (Finset.univ.sum fun a => ψ a) = ↑(Fintype.card R)
This theorem is stating that for any type `R` that has an additive group structure and is finite (given by `Fintype R`), and for any commutative ring `R'`, if we have an additive character `ψ : AddChar R R'` that is trivial (i.e., not nontrivial), then the sum of the values of this character over all elements of `R` is equal to the number of elements in `R`. This is expressed as the cardinality of `R`, denoted by `Fintype.card R`. In mathematical terms, this theorem asserts that $\sum_{a \in R} \psi(a) = \lvert R \rvert$ when `ψ` is a trivial additive character.
More concisely: For any finite additive group `R` with a trivial additive character `ψ : AddChar R R'`, we have the equality of sums: $\sum\_{a \in R} \psi(a) = \lvert R \rvert$.
|