Theorem ZMod.pow_card_sub_one

feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843) …

feat: `a ^ (p - 1) = if a ≠ 0 then 1 else 0` in `ZMod p` (#13828) …