MulChar.ofUnitHom_coe
theorem MulChar.ofUnitHom_coe :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ),
(MulChar.ofUnitHom f) ↑a = ↑(f a)
The theorem `MulChar.ofUnitHom_coe` states that for any two types `R` and `R'` where `R` is a commutative monoid and `R'` is a commutative monoid with zero, a homomorphism `f` from the group of units of `R` to the group of units of `R'`, and a unit `a` of `R`, applying the function `MulChar.ofUnitHom` to the homomorphism `f` and then applying the resulting function to the canonical embedding of `a` in `R` is equal to the canonical embedding of `f a` in `R'`. In other words, the function `MulChar.ofUnitHom` preserves the action of the homomorphism `f` on the units of `R`.
More concisely: Given commutative monoids R and R' with zero, a homomorphism f from the group of units of R to the group of units of R', and a unit a in R, the application of MulChar.ofUnitHom to f and then to the canonical embedding of a in R equals the canonical embedding of f(a) in R'.
|
MulChar.IsQuadratic.sq_eq_one
theorem MulChar.IsQuadratic.sq_eq_one :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {χ : MulChar R R'},
χ.IsQuadratic → χ ^ 2 = 1
This theorem states that the square of a quadratic character is the trivial character. Here, for any commutative monoid 'R', any commutative ring 'R'', and any multiplicative character 'χ' from 'R' to 'R'', if 'χ' is a quadratic character, then 'χ' squared is equal to 1. This can be interpreted as saying that the operation of squaring a quadratic character returns the trivial (identity) character in the context of multiplicative characters in number theory.
More concisely: If 'χ' is a quadratic character from a commutative ring 'R' to another commutative ring 'R'' then 'χ'^2 = 1.
|
MulChar.inv_apply
theorem MulChar.inv_apply :
∀ {R' : Type v} [inst : CommMonoidWithZero R'] {R : Type u} [inst_1 : CommMonoidWithZero R] (χ : MulChar R R')
(a : R), χ⁻¹ a = χ (Ring.inverse a)
The theorem `MulChar.inv_apply` states that in a commutative monoid with zero (`CommMonoidWithZero`) denoted as `R` and another commutative monoid with zero (`CommMonoidWithZero`) denoted as `R'`, for any multiplicative character `χ` from `R` to `R'` and any element `a` from `R`, the inverse of `χ` applied to `a` is equal to `χ` applied to the inverse of `a`. This is to say, for a multiplicative character and an element from the domain, applying the inverse of the character to the element is the same as applying the character to the inverse of the element.
More concisely: For any commutative monoid with zero `R`, any commutative monoid with zero `R'`, any multiplicative character `χ : R → R'`, and any element `a ∈ R`, `χ(-a) = -(χ(a))`.
|
MulChar.pow_apply'
theorem MulChar.pow_apply' :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') {n : ℕ},
n ≠ 0 → ∀ (a : R), (χ ^ n) a = χ a ^ n
This theorem states that for any positive natural number `n`, for any elements `a` of a commutative monoid `R` and `χ` of a certain mapping called `MulChar` from `R` to another commutative monoid with zero `R'`, the `n`th power of the function `χ` applied to `a` is equal to the function `χ` applied to `a` raised to the `n`th power. In mathematical notation, if `n` is positive, then `(χ ^ n) a = (χ a) ^ n`.
More concisely: For any commutative monoid with zero `R`, any mapping `χ` from `R` to another commutative monoid with zero `R'` called `MulChar`, and any positive natural number `n`, the `n`th power of `χ` applied to an element `a` in `R` equals `χ` applied to `a` raised to the power of `n`, i.e., `(χ ^ n) a = (χ a) ^ n`.
|
MulChar.pow_apply_coe
theorem MulChar.pow_apply_coe :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (n : ℕ)
(a : Rˣ), (χ ^ n) ↑a = χ ↑a ^ n
This theorem states that for any commutative monoid `R`, commutative monoid with zero `R'`, multiplicative character `χ` from `R` to `R'`, natural number `n`, and unit `a` of `R`, the `n`th power of `χ` applied to `a` equals the `n`th power of `χ` applied to `a`. In other words, raising a multiplicative character to a power and then applying it to a unit is the same as applying the character to the unit first and then raising the result to the power.
More concisely: For any commutative monoids R and R' with zero, multiplicative character χ from R to R', natural number n, and unit a of R, χ^n(a) = χ(a)^n.
|
MulChar.IsQuadratic.pow_odd
theorem MulChar.IsQuadratic.pow_odd :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {χ : MulChar R R'},
χ.IsQuadratic → ∀ {n : ℕ}, Odd n → χ ^ n = χ
The theorem `MulChar.IsQuadratic.pow_odd` states that for any commutative monoid `R`, any commutative ring `R'`, and any multiplicative character `χ` from `R` to `R'` that is quadratic, if `n` is an odd natural number (i.e., if there exists a natural number `k` such that `n = 2*k + 1`), then the `n`-th power of `χ` is equal to `χ`.
More concisely: If `χ` is a quadratic multiplicative character on the commutative monoid/ring `R`, then `χ(n) = χ^(2*k+1) = χ` for some natural number `k`, i.e., for odd natural numbers `n`.
|
MulChar.map_nonunit
theorem MulChar.map_nonunit :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') {a : R},
¬IsUnit a → χ a = 0
The theorem `MulChar.map_nonunit` states that for any two types `R` and `R'` which are Commutative Monoids, and `R'` further has an operation `zero`, if `χ` is a mapping (referred to as `MulChar`) from `R` to `R'`, then for any element `a` of `R` that is not a unit (i.e., does not have a two-sided inverse in `R`), the mapping `χ` will map `a` to `0` in `R'`.
More concisely: If `χ: R → R'` is a mapping between commutative monoids `R` and `R'` with identity `zero` in `R'`, and `a` is a non-unit in `R`, then `χ(a) = 0`.
|
MulChar.inv_apply_eq_inv'
theorem MulChar.inv_apply_eq_inv' :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : Field R'] (χ : MulChar R R') (a : R),
χ⁻¹ a = (χ a)⁻¹
This theorem states that for any multiplicative character `χ` from a commutative monoid `R` to a field `R'` and any element `a` in `R`, the inverse of `χ` applied to `a` is equal to the inverse of applying `χ` to `a`. In other words, inverting the function before applying it to `a` is the same as applying the function to `a` first and then taking the inverse.
More concisely: For any commutative monoid homomorphism of multiplicative characters χ : R → F (where R is a commutative monoid and F is a field), and for any element a in R, χ(-a) = (χ(a))^-1.
|
MulChar.inv_mul
theorem MulChar.inv_mul :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'),
χ⁻¹ * χ = 1
This theorem states that for any types `R` and `R'` that are commutative monoids, and for `R'` also having an additional property of having a zero, and given a multiplicative character `χ` from `R` to `R'`, the product of this character and its inverse equals to the trivial character, which is represented by `1`. In more mathematical terms, if `χ` is a character of a commutative monoid `R` into `R'`, then `χ^-1 * χ = 1`.
More concisely: Given a commutative monoid `R` with unit, and a character `χ : R → R'` to another commutative monoid `R'` with zero, `χ^-1 * χ = 1`.
|
MulChar.IsNontrivial.sum_eq_zero
theorem MulChar.IsNontrivial.sum_eq_zero :
∀ {R : Type u} [inst : CommMonoid R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R']
[inst_3 : IsDomain R'] {χ : MulChar R R'}, χ.IsNontrivial → (Finset.univ.sum fun a => χ a) = 0
The theorem `MulChar.IsNontrivial.sum_eq_zero` states that for any finite commutative monoid `R`, any commutative ring `R'` which is also a domain, and any nontrivial multiplicative character `χ` from `R` to `R'`, the sum of the values of `χ` over all elements in `R` is zero. This is a statement about the structure of finite rings and their multiplicative characters, which are functions preserving multiplication.
More concisely: For any finite commutative monoid R, commutative ring R' being a domain, and nontrivial multiplicative character χ from R to R', the sum of χ over all elements in R equals zero.
|
MulChar.coe_toUnitHom
theorem MulChar.coe_toUnitHom :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ),
↑(χ.toUnitHom a) = χ ↑a
The theorem `MulChar.coe_toUnitHom` states that for any two types `R` and `R'` with `R` a commutative monoid and `R'` a commutative monoid with zero, for any multiplication character `χ` from `R` to `R'` and any unit `a` of `R`, the application of the `MulChar.toUnitHom` function to `χ` and `a` followed by coercing the result to `R'` is equivalent to directly applying `χ` to the coercion of `a` to `R`. In other words, the `MulChar.toUnitHom` function maintains the behavior of the multiplication character when applied to units of the commutative monoid `R`.
More concisely: For any commutative monoids R and R' with zero, multiplication character χ from R to R', and unit a of R, the application of χ to the coercion of a to R' is equal to the application of MulChar.toUnitHom(χ, a) to the zero of R'.
|
MulChar.equivToUnitHom_symm_coe
theorem MulChar.equivToUnitHom_symm_coe :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ),
(MulChar.equivToUnitHom.symm f) ↑a = ↑(f a)
This theorem states that for all commutative monoids `R` and `R'` (where `R'` has a zero element), and for all homomorphisms `f` from the units of `R` to the units of `R'`, and any unit `a` of `R`, if we apply the inverse of the equivalence `MulChar.equivToUnitHom` to `f` and then apply the result to the coercion of `a` (which implicitly converts `a` from a unit to a general element of `R`), it is equivalent to applying `f` to `a` and then coercing the result to a general element of `R'`. This theorem essentially states that the equivalence `MulChar.equivToUnitHom` preserves the behavior of the homomorphism `f` and its interaction with the coercion operation.
More concisely: For all commutative monoids `R` and `R'`, homomorphisms `f` from the units of `R` to the units of `R'`, and units `a` of `R`, the application of `f.to_fun` followed by coercion from `R` to `R'` is equal to the application of `f` to `a` and coercion from `R` to `R'`. (Here, `f.to_fun` denotes the function component of the homomorphism `f`.)
|
MulChar.IsQuadratic.pow_char
theorem MulChar.IsQuadratic.pow_char :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {χ : MulChar R R'},
χ.IsQuadratic → ∀ (p : ℕ) [hp : Fact p.Prime] [inst_2 : CharP R' p], χ ^ p = χ
This theorem states that for any commutative monoid `R`, any commutative ring `R'`, any multiplicative character (map) `χ` from `R` to `R'`, and any prime number `p`, if `χ` is a quadratic character (meaning that the square of `χ` is the trivial character) and `p` is the characteristic of the ring `R'`, then raising `χ` to the power of `p` yields `χ` itself. The characteristic of a ring is a prime number `p` if every sum of `p` ones is zero in the ring.
More concisely: For any commutative monoid `R`, commutative ring `R'`, multiplicative character `χ` from `R` to `R'`, and prime number `p` equal to the characteristic of `R'`, if `χ` is a quadratic character then `χ^p = χ`.
|
MulChar.map_ringChar
theorem MulChar.map_ringChar :
∀ {R' : Type v} [inst : CommMonoidWithZero R'] {R : Type u} [inst_1 : CommRing R] [inst_2 : Nontrivial R]
(χ : MulChar R R'), χ ↑(ringChar R) = 0
The theorem `MulChar.map_ringChar` states that for all types `R'` and `R`, where `R'` is a commutative monoid with zero and `R` is a commutative ring that is nontrivial, given a multiplicative characteristic (`MulChar`) `χ` from `R` to `R'`, the value of `χ` applied to the ring characteristic of `R` (`ringChar R`) is zero. In other words, this theorem states that the multiplicative characteristic map sends the ring characteristic of any nontrivial commutative ring to zero.
More concisely: For any commutative ring R that is nontrivial and any multiplicative characteristic map χ from R to a commutative monoid with zero, χ(ringChar R) = 0.
|
MulChar.IsQuadratic.eq_of_eq_coe
theorem MulChar.IsQuadratic.eq_of_eq_coe :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {R'' : Type w} [inst_2 : CommRing R'']
{χ : MulChar R ℤ},
χ.IsQuadratic →
∀ {χ' : MulChar R' ℤ},
χ'.IsQuadratic →
∀ [inst_3 : Nontrivial R''], ringChar R'' ≠ 2 → ∀ {a : R} {a' : R'}, ↑(χ a) = ↑(χ' a') → χ a = χ' a'
This theorem states that if two quadratic characters, with values in the set of integers (`ℤ`), agree after being coerced into a ring whose characteristic is not `2`, then they also agree in the set of integers (`ℤ`). More specifically, given two types `R` and `R'` with their associated commutative monoid and ring structures, respectively, and another type `R''` with a commutative ring structure, if we have two quadratic multiplicative characters `χ` and `χ'`, mapping from `R` and `R'` to `ℤ` respectively, and the ring `R''` is nontrivial with a characteristic not equal to `2`, then if the coerced values of `χ a` and `χ' a'` are equal, it implies that `χ a` equals `χ' a'` in `ℤ`.
More concisely: If two quadratic characters from commutative rings with characteristic not equal to 2 agree after coercion to a nontrivial commutative ring, then they agree as integer-valued functions.
|
MulChar.sum_one_eq_card_units
theorem MulChar.sum_one_eq_card_units :
∀ {R : Type u} [inst : CommMonoid R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R']
[inst_3 : DecidableEq R], (Finset.univ.sum fun a => 1 a) = ↑(Fintype.card Rˣ)
This theorem states that for any finite commutative ring `R` and any commutative monoid `R'` with decidable equality on `R`, the sum of the value 1 computed over all elements of `R` (i.e., the total number of elements in `R`) is equal to the number of units (invertible elements) in `R`. This is represented by `Fintype.card Rˣ`, where `Rˣ` denotes the multiplicative group of units in `R`.
More concisely: The number of units in a finite commutative ring is equal to the cardinality of the ring.
|
MulChar.map_zero
theorem MulChar.map_zero :
∀ {R' : Type v} [inst : CommMonoidWithZero R'] {R : Type u} [inst_1 : CommMonoidWithZero R] [inst_2 : Nontrivial R]
(χ : MulChar R R'), χ 0 = 0
This theorem, known as `MulChar.map_zero`, states that for any two types `R'` and `R` that are commutative monoids with a zero element, and where `R` is nontrivial, if `χ` is a multiplication character from `R` to `R'`, then the value of this character at zero is zero. In mathematical terms, if `χ` is a function which respects multiplication in `R` and `R'`, i.e., `χ(ab) = χ(a)χ(b)`, then `χ(0) = 0`.
More concisely: If `χ` is a multiplication character from a commutative monoid `R` with a zero element, where `R` is nontrivial, then `χ(0) = 0`.
|
MulChar.inv_apply'
theorem MulChar.inv_apply' :
∀ {R' : Type v} [inst : CommMonoidWithZero R'] {R : Type u} [inst_1 : Field R] (χ : MulChar R R') (a : R),
χ⁻¹ a = χ a⁻¹
This theorem states that for any commutative monoid with zero `R'`, any field `R`, any multiplicative character `χ` from `R` to `R'`, and any element `a` from `R`, the inverse of `χ` applied to `a` is equal to `χ` applied to the inverse of `a`.
To put it simply, it is showing that the inverse operation on a multiplicative character is equivalent to applying the character to the inverse of an element in the field.
More concisely: For any commutative monoid with zero `R` having a field of scalars `R'`, any multiplicative character `χ : R → R'`, and any element `a ∈ R`, `χ(-a) = χ(a)^-1`.
|
MulChar.IsQuadratic.pow_even
theorem MulChar.IsQuadratic.pow_even :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {χ : MulChar R R'},
χ.IsQuadratic → ∀ {n : ℕ}, Even n → χ ^ n = 1
The theorem `MulChar.IsQuadratic.pow_even` states that for any type `R` that is a commutative monoid, any type `R'` that is a commutative ring, and any multiplicative character `χ` from `R` to `R'` that is quadratic, if `n` is an even natural number, then the `n`th power of the multiplicative character `χ` is equal to the trivial character, which is represented by `1`. In other words, raising a quadratic multiplicative character to an even power results in the trivial character.
More concisely: For any commutative ring `R'`, commutative monoid `R`, multiplicative character `χ` from `R` to `R'` that is quadratic, the equality `χ ^ (2n) = 1` holds for all even natural numbers `n`.
|
MulChar.ext'
theorem MulChar.ext' :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] {χ χ' : MulChar R R'},
(∀ (a : R), χ a = χ' a) → χ = χ'
This theorem, named `MulChar.ext'`, is about the extensionality of Multiplicative Characters (`MulChar`). If two Multiplicative Characters, `χ` and `χ'`, from a commutative monoid `R` to a commutative monoid with zero `R'`, produce the same output for all elements of `R`, then they are equal. In other words, if for every element `a` in `R`, `χ a` equals `χ' a`, then `χ` equals `χ'`. This is typically used to show that two function-like objects are the same if they behave the same way on all possible inputs.
More concisely: If two multiplicative characters from commutative monoids to commutative monoids with zero produce the same output for all elements, then they are equal.
|
MulChar.IsQuadratic.inv
theorem MulChar.IsQuadratic.inv :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {χ : MulChar R R'},
χ.IsQuadratic → χ⁻¹ = χ
This theorem states that for any commutative monoid `R`, any commutative ring `R'`, and any multiplicative character `χ` from `R` to `R'`, if `χ` is a quadratic character, then its inverse is equal to itself. In other words, the inverse of a quadratic multiplicative character on a commutative monoid is the character itself.
More concisely: For any commutative monoid `R`, any commutative ring `R'`, and any quadratic multiplicative character `χ` from `R` to `R'`, `χ` is its own inverse.
|
MulChar.one_apply_coe
theorem MulChar.one_apply_coe :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (a : Rˣ), 1 ↑a = 1
This theorem states that for any commutative monoid `R` and any commutative monoid with zero `R'`, if you take any element `a` from the group of units of `R`, then applying the trivial character (which is represented by the constant `1`) to `a` (notated as `1 ↑a`) always results in `1`. In other words, the trivial character maps all elements of the group of units to `1`.
More concisely: For any commutative monoids `R` and `R'` with zero, and for any unit `a` in `R`, the trivial character `1` maps `a` to the identity element `1` in `R'`.
|
MulChar.ext
theorem MulChar.ext :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] {χ χ' : MulChar R R'},
(∀ (a : Rˣ), χ ↑a = χ' ↑a) → χ = χ'
The theorem `MulChar.ext` is a statement about extensionality in the context of multiplication characters (MulChar). Given two types `R` and `R'`, where `R` is a commutative monoid and `R'` is a commutative monoid with zero, and two multiplication characters `χ` and `χ'` from `R` to `R'`, if those characters coincide on the multiplicative units (`Rˣ`) of `R`, then the characters `χ` and `χ'` are equal. This comes from the fact that multiplication characters always map non-units to zero, so you only need to compare the values on units to determine if two multiplication characters are the same.
More concisely: If two multiplication characters from a commutative monoid to a commutative monoid with zero have the same value on the multiplicative units, then they are equal.
|
MulChar.inv_apply_eq_inv
theorem MulChar.inv_apply_eq_inv :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (a : R),
χ⁻¹ a = Ring.inverse (χ a)
The theorem `MulChar.inv_apply_eq_inv` asserts that for any commutative monoid `R`, any commutative monoid with zero `R'`, any multiplicative character `χ` from `R` to `R'`, and any element `a` of `R`, the inverse of the multiplicative character `χ` applied to `a` is equal to the Ring's inverse of the character `χ` evaluated at `a`. In other words, if we apply the inverse operation to the character `χ` and then apply this to `a`, we get the same result as if we first apply the character `χ` to `a` and then take the inverse in the ring structure of `R'`.
More concisely: For any commutative monoids R and R' with zero, commutative multiplicative character χ from R to R', and element a in R, χ^-1(a) = χ^(-1) a, where χ^-1 is the inverse of χ as a function and χ^(-1) is the multiplicative inverse of χ in R'.
|
MulChar.IsQuadratic.comp
theorem MulChar.IsQuadratic.comp :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {R'' : Type w} [inst_2 : CommRing R'']
{χ : MulChar R R'}, χ.IsQuadratic → ∀ (f : R' →+* R''), (χ.ringHomComp f).IsQuadratic
The theorem states that if you have a quadratic character (a specific type of function) from a commutative monoid to a commutative ring, and if you compose this function with a ring homomorphism (a function that preserves the ring structure), the resulting function is also a quadratic character. This holds true for any commutative monoid, and any two commutative rings.
More concisely: If f is a quadratic character from a commutative monoid M to a commutative ring R, and g is a ring homomorphism from ring S to R, then the composite function f ∘ g is a quadratic character from M to S.
|
MulChar.IsNontrivial.comp
theorem MulChar.IsNontrivial.comp :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommRing R'] {R'' : Type w} [inst_2 : CommRing R'']
{χ : MulChar R R'}, χ.IsNontrivial → ∀ {f : R' →+* R''}, Function.Injective ⇑f → (χ.ringHomComp f).IsNontrivial
The theorem `MulChar.IsNontrivial.comp` states that for any types `R`, `R'`, and `R''`, where `R` is a commutative monoid and `R'` and `R''` are commutative rings, given a multiplicative characteristic function `χ` from `R` to `R'` that is nontrivial, and a ring homomorphism `f` from `R'` to `R''` that is injective, the multiplicative characteristic function obtained by composing `χ` and `f` is also nontrivial. Here, a function is nontrivial if it does not map all elements to a single value, and a function is injective if distinct inputs always result in distinct outputs.
More concisely: If `χ: R → R'` is a nontrivial multiplicative characteristic function from a commutative monoid `R` to a commutative ring `R'`, and `f: R' → R''` is an injective ring homomorphism from `R'` to another commutative ring `R''`, then the composed function `χ ∘ f: R → R''` is also a nontrivial multiplicative characteristic function.
|
MulChar.isNontrivial_iff
theorem MulChar.isNontrivial_iff :
∀ {R : Type u} [inst : CommMonoid R] {R' : Type v} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'),
χ.IsNontrivial ↔ χ ≠ 1
This theorem states that a multiplicative character, denoted as `χ`, is nontrivial if and only if it is not equivalent to the trivial character (represented as `1`). This equivalence holds for any commutative monoid `R` and any commutative monoid with zero `R'`. The multiplicative character `χ` is a function from `R` to `R'`. In other words, a multiplicative character is considered nontrivial exactly when it is different from the trivial character.
More concisely: A multiplicative character `χ` from a commutative monoid `R` to a commutative monoid with zero `R'` is nontrivial if and only if it is not equivalent to the trivial character `1`.
|