Finite fields and groups with zero

Basic results about powers and inverses in finite groups with zero and finite fields.

Main results

• FiniteField.pow_card_sub_two_eq_inv: in a finite group with zero K, a ^ (q - 2) = a⁻¹ for a ≠ 0.
• ZMod.pow_card_sub_two_eq_inv: Fermat's inverse identity a ^ (p - 2) = a⁻¹ in ZMod p.

theorem FiniteField.pow_card_sub_two_eq_inv {K : Type u_1} [GroupWithZero K] [Fintype K] (a : K) (ha : a ≠ 0) : a ^ (Fintype.card K - 2) = a⁻¹

In a finite group with zero, the q - 2-nd power of a nonzero element is its inverse.

theorem ZMod.pow_card_sub_two_eq_inv {p : ℕ} [Fact (Nat.Prime p)] {a : ZMod p} (ha : a ≠ 0) : a ^ (p - 2) = a⁻¹

In ZMod p, the p - 2-nd power of a nonzero residue is its inverse.