Nonzero elements of a field with a nontrivial power

A field with more than k + 1 elements has a nonzero element whose k-th power is not one, for every positive k: the field is finite, its unit group is cyclic of order Nat.card F - 1 > k, and a generator has order larger than k. For k = 2 and fields with at least four elements this is the input to the perfectness of the special linear groups in rank two.

Main results

• TauCeti.FiniteField.exists_ne_zero_pow_ne_one: a field with more than k + 1 elements has a nonzero element a with a ^ k ≠ 1.

theorem TauCeti.FiniteField.exists_ne_zero_pow_ne_one {F : Type u_1} [Field F] {k : ℕ} (hk : k ≠ 0) (hF : k + 1 < Nat.card F) : ∃ (a : F), a ≠ 0 ∧ a ^ k ≠ 1

A field with more than k + 1 elements has a nonzero element whose k-th power is not one, for every positive k. Such a field is finite with a cyclic unit group of order larger than k, so this is exists_pow_ne_one_of_isCyclic.