Powers equal to -1 of an element of even order

Let u be an element of order 2 * m, with m ≠ 0, in a ring without zero divisors. Then u ^ m squares to 1 and is not 1, so it is -1, the only other square root of 1. Since the powers of u repeat with period 2 * m, the exponents k with u ^ k = -1 are exactly the odd multiples of m: those with m ∣ k and ¬ 2 * m ∣ k.

The hypothesis that there are no zero divisors is needed: in ZMod 8 the residue 3 has order 2 but is not -1. In characteristic two no element has even order, since -1 = 1.

Applied to residues modulo a prime, this decides which q ^ k + 1 the prime divides from the multiplicative order of q.

Main results

• TauCeti.pow_eq_neg_one_of_orderOf_eq_two_mul: if orderOf u = 2 * m and m ≠ 0, then u ^ m = -1.
• TauCeti.pow_eq_neg_one_iff_of_orderOf_eq_two_mul: if orderOf u = 2 * m and m ≠ 0, then u ^ k = -1 if and only if m ∣ k and ¬ 2 * m ∣ k.

theorem TauCeti.pow_eq_neg_one_of_orderOf_eq_two_mul {R : Type u_1} [Ring R] [NoZeroDivisors R] {u : R} {m : ℕ} (hu : orderOf u = 2 * m) (hm : m ≠ 0) : u ^ m = -1

In a ring without zero divisors, an element of order 2 * m with m ≠ 0 has m-th power -1.

theorem TauCeti.pow_eq_neg_one_iff_of_orderOf_eq_two_mul {R : Type u_1} [Ring R] [NoZeroDivisors R] {u : R} {m : ℕ} (hu : orderOf u = 2 * m) (hm : m ≠ 0) (k : ℕ) : u ^ k = -1 ↔ m ∣ k ∧ ¬2 * m ∣ k

In a ring without zero divisors, if u has order 2 * m with m ≠ 0, then u ^ k = -1 exactly for the odd multiples k of m.