Powers indexed by residues

If x ^ n = 1 in a monoid, then the power x ^ a.val of x at the canonical representative of a residue a : ZMod n is multiplicative in a. At n = 2 and x = -1 this is the sign (-1) ^ a.val of a residue modulo two.

Main results

• TauCeti.pow_val_add: x ^ (a + b).val = x ^ a.val * x ^ b.val when x ^ n = 1.

theorem TauCeti.pow_val_add {M : Type u_1} [Monoid M] {n : ℕ} [NeZero n] {x : M} (hx : x ^ n = 1) (a b : ZMod n) : x ^ (a + b).val = x ^ a.val * x ^ b.val

A power indexed by a residue is multiplicative in the residue: if x ^ n = 1, then x ^ (a + b).val = x ^ a.val * x ^ b.val for a b : ZMod n.