AddChar.mulShift_zero
theorem AddChar.mulShift_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M), ψ.mulShift 0 = 1 := by
sorry
This theorem states that for any additive character `ψ` of a ring `R` with a commutative monoid `M`, the operation `mulShift` applied to `ψ` with `0` yields `1`. In other words, the `mulShift` operation of `0` on any additive character is equivalent to the trivial character in the context of ring and commutative monoid.
More concisely: For any additive character `ψ` of a commutative monoid in a ring, `ψ(0)` is the trivial character under the `mulShift` operation.
|
AddChar.mulShift_spec'
theorem AddChar.mulShift_spec' :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (n : ℕ) (x : R),
(ψ.mulShift ↑n) x = ψ x ^ n
This theorem states that for any ring `R`, commutative monoid `M`, additive characteristic map `ψ` from `R` to `M`, natural number `n`, and element `x` of `R`, the result of applying the `mulShift` function of `ψ` to `n` and `x` is equal to the result of raising the output of `ψ` applied to `x` to the power of `n`. In other words, in terms of mathematical notation, if `n` is a natural number, then `mulShift ψ n x = (ψ x) ^ n`.
More concisely: For any commutative monoid `M`, additive characteristic map `ψ` from a ring `R` to `M`, and natural number `n`, the function `mulShift ψ` applied to `n` and an element `x` from `R` equals the `n`th power of the element `ψ(x)` in `M`.
|
AddChar.inv_mulShift
theorem AddChar.inv_mulShift :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M), ψ⁻¹ = ψ.mulShift (-1)
The theorem `AddChar.inv_mulShift` states that for any ring `R`, commutative monoid `M`, and additive character `ψ` from `R` to `M`, the inverse of `ψ` is equivalent to calling the `mulShift` function on `ψ` with `-1` as the shift parameter. This theorem holds for all types `R` and `M` that meet these conditions.
More concisely: For any commutative monoid `M`, additive character `ψ` from a ring `R` to `M`, the inverse of `ψ` is equal to the `mulShift` function applied to `ψ` with a shift parameter of `-1`.
|
AddChar.map_nsmul_pow
theorem AddChar.map_nsmul_pow :
∀ {A : Type u_1} {M : Type u_2} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (n : ℕ) (x : A),
ψ (n • x) = ψ x ^ n
This theorem, titled `AddChar.map_nsmul_pow`, states that for any types `A` and `M`, where `A` is an additive monoid and `M` is a monoid, any additive character `ψ` from `A` to `M`, any natural number `n`, and any element `x` of `A`, the additive character applied to `n` "copies" of `x` (denoted by `n • x`) equals the additive character applied to `x`, raised to the power `n`. This essentially states that an additive character maps multiples of an element into powers of the character's output for that element.
More concisely: For any additive monoid `A`, monoid `M`, additive character `ψ` from `A` to `M`, natural number `n`, and element `x` of `A`, `ψ(n • x) = ψ(x)^n`.
|
AddChar.ext
theorem AddChar.ext :
∀ {A : Type u_1} {M : Type u_2} [inst : AddMonoid A] [inst_1 : Monoid M] (f g : AddChar A M),
(∀ (x : A), f x = g x) → f = g
This theorem, `AddChar.ext`, states that for any two `AddChar` (additive characters) `f` and `g` from a type `A` to a type `M`, where `A` is an additive monoid and `M` is a monoid, if `f` and `g` give the same value for all elements in `A`, then `f` and `g` are considered equal. In other words, it's a proof of the extensionality of additive characters, asserting that two additive character functions are identical if they map every element of their domain to the same element in their codomain.
More concisely: If two additive characters `f` and `g` from an additive monoid `A` to a monoid `M` agree on all elements of `A`, then `f` is equal to `g`.
|
AddChar.isNontrivial_iff_ne_trivial
theorem AddChar.isNontrivial_iff_ne_trivial :
∀ {A : Type u_1} {M : Type u_2} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M),
ψ.IsNontrivial ↔ ψ ≠ 1
This theorem states that for any given additive character `ψ`, which is a map from an additive monoid `A` to a monoid `M`, the character is nontrivial (meaning it has some interesting or complex structure) if and only if it is not the trivial character (represented as `1`). Essentially, it's a way of characterizing the nontriviality of additive characters in terms of not being the simplest possible character.
More concisely: A additive character ψ from an additive monoid A to a monoid M is nontrivial if and only if it is not the trivial character (i.e., not the identity function).
|
AddChar.map_zero_one
theorem AddChar.map_zero_one :
∀ {A : Type u_1} {M : Type u_2} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M), ψ 0 = 1
This theorem states that for any additive character `ψ` from a type `A` which is an additive monoid, to a type `M` which is a monoid, the value of `ψ` at `0` is `1`. In other words, an additive character always maps the additive identity (which is `0` in this context) to the multiplicative identity (which is `1`).
More concisely: For any additive character ψ from an additive monoid A to a monoid M, ψ(0) = 1.
|
AddChar.mulShift_apply
theorem AddChar.mulShift_apply :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] {ψ : AddChar R M} {r x : R},
(ψ.mulShift r) x = ψ (r * x)
This theorem states that for any ring `R`, commutative monoid `M`, additive character `ψ : AddChar R M`, and elements `r` and `x` of `R`, the application of `AddChar.mulShift` to `ψ` and `r`, and then to `x`, is equal to the application of `ψ` to the product of `r` and `x`. In other words, shifting the additive character `ψ` by multiplication with `r`, and then applying it to `x`, results in the same value as directly applying `ψ` to the product of `r` and `x`.
More concisely: For any commutative monoid `M`, additive character `ψ : AddChar R M`, and ring elements `r, x` of `R`, `AddChar.mulShift ψ r x = ψ (r * x)`.
|
AddChar.mulShift_mul
theorem AddChar.mulShift_mul :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (r s : R),
ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)
This theorem states that for any ring `R`, commutative monoid `M`, additive character `ψ` of ring `R` to `M`, and any two elements `r` and `s` from `R`, the product of `ψ.mulShift r` and `ψ.mulShift s` is equal to `ψ.mulShift` of the sum of `r` and `s`. It is essentially showing the distributive property of multiplication over addition in this specific context.
More concisely: For any commutative monoid `M`, additive character `ψ` of ring `R`, and all elements `r` and `s` in `R`, we have `ψ.mulShift (r + s) = ψ.mulShift r * ψ.mulShift s`.
|
AddChar.map_add_mul
theorem AddChar.map_add_mul :
∀ {A : Type u_1} {M : Type u_2} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M) (x y : A),
ψ (x + y) = ψ x * ψ y
This theorem states that for any given additive character `ψ` defined over an additive monoid `A` and a monoid `M`, the character value of the sum of two elements `x` and `y` from `A` is equal to the product of the character values of `x` and `y` individually. In mathematical terms, this can be written as `ψ (x + y) = ψ x * ψ y`. The theorem encapsulates one of the fundamental properties of additive characters, namely their ability to map addition in the domain to multiplication in the codomain.
More concisely: For any additive character ψ over an additive monoid A and all elements x, y from A, ψ (x + y) = ψ x * ψ y.
|
AddChar.pow_mulShift
theorem AddChar.pow_mulShift :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (n : ℕ),
ψ ^ n = ψ.mulShift ↑n
This theorem states that for any natural number `n` and any character `ψ` in a ring `R` with commutative monoid `M`, the `n`-th power of `ψ` is equal to the result of the `mulShift` operation on `ψ` with `n` as the argument. In the context of number theory, `AddChar` is used to represent additive characters, so this theorem relates the exponentiation of additive characters to a shift operation within the ring.
More concisely: For any natural number `n` and additive character `ψ` in a commutative ring `R`, the `n`-th power of `ψ` equals the `mulShift` operation applied `n` times to `ψ` in `R`.
|
AddChar.map_zsmul_zpow
theorem AddChar.map_zsmul_zpow :
∀ {A : Type u_1} {M : Type u_2} [inst : AddGroup A] [inst_1 : DivisionMonoid M] (ψ : AddChar A M) (n : ℤ) (a : A),
ψ (n • a) = ψ a ^ n
This theorem, `AddChar.map_zsmul_zpow`, states that for any given types `A` and `M`, where `A` is an additive group and `M` is a division monoid, an additive character `ψ` mapping from `A` to `M` has the property that the additive character of an integer scalar multiple of an element from `A` is equal to the integer power of the additive character of that element. In other words, for any integer `n` and any element `a` of `A`, `ψ(n • a) = ψ(a)^n`.
More concisely: For any additive character ψ from an additive group A to a division monoid M, ψ(n * a) = ψ(a)^n for all integers n and elements a in A.
|