Euler's criterion for n-th powers in a finite field

Let F be a finite field with q elements and n ∣ q - 1. A nonzero a ∈ F is an n-th power exactly when a ^ ((q - 1) / n) = 1. At n = 2 this is Mathlib's FiniteField.isSquare_iff (in odd characteristic).

Main results

• TauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one: Euler's criterion for n-th powers in a finite field.

theorem TauCeti.FiniteField.exists_pow_eq_iff_pow_card_sub_one_div_eq_one {F : Type u_1} [Field F] [Finite F] {n : ℕ} (hn : n ∣ Nat.card F - 1) {a : F} (ha : a ≠ 0) : (∃ (b : F), b ^ n = a) ↔ a ^ ((Nat.card F - 1) / n) = 1

Euler's criterion in a finite field. If n ∣ #F - 1, then a nonzero a ∈ F is an n-th power exactly when a ^ ((#F - 1) / n) = 1.