Eigenvectors of right multiplication by a monoid element

Let g be an element of a monoid G and c a scalar of a commutative ring R. A nonzero element x of the monoid algebra R[G] with x (g - c) = 0 is an eigenvector of right multiplication by g with eigenvalue c. When g has finite order, right multiplication by g ^ orderOf g = 1 is the identity, so when R has no zero divisors the eigenvalue is a root of unity of order dividing orderOf g. The equality c ^ orderOf g = 1 also holds when g has infinite order, but is then vacuous because orderOf g = 0. In characteristic zero the only natural number that is such a root of unity is 1.

Main statements

• TauCeti.pow_orderOf_eq_one_of_mul_single_sub_eq_zero: the eigenvalue c satisfies c ^ orderOf g = 1.
• TauCeti.nat_eq_one_of_mul_single_sub_eq_zero: in characteristic zero, a natural-number eigenvalue of an element of finite order is 1.

theorem TauCeti.pow_orderOf_eq_one_of_mul_single_sub_eq_zero {R : Type u_1} [CommRing R] [NoZeroDivisors R] {G : Type u_2} [Monoid G] {x : MonoidAlgebra R G} (hx : x ≠ 0) {g : G} {c : R} (h : x * (MonoidAlgebra.single g 1 - MonoidAlgebra.single 1 c) = 0) : c ^ orderOf g = 1

If a nonzero element x of R[G] satisfies x (g - c) = 0, then c ^ orderOf g = 1.

theorem TauCeti.nat_eq_one_of_mul_single_sub_eq_zero {R : Type u_1} [CommRing R] [NoZeroDivisors R] {G : Type u_2} [Monoid G] [CharZero R] {x : MonoidAlgebra R G} (hx : x ≠ 0) {g : G} (hg : IsOfFinOrder g) {a : ℕ} (h : x * (MonoidAlgebra.single g 1 - MonoidAlgebra.single 1 ↑a) = 0) : a = 1

In characteristic zero, if a nonzero element x of R[G] satisfies x (g - a) = 0 for an element g of finite order and a natural number a, then a = 1.