Commit 2025-01-20 15:19 fb0f8faf

View on Github →

chore(Algebra/CharP): prime_ringChar and isPrimePow_card (#20860) small helper lemmas that didn't exist for finite fields

Estimated changes

Modified Mathlib/Algebra/CharP/Lemmas.lean

added theorem CharP.prime_ringChar

Modified Mathlib/FieldTheory/Finite/Basic.lean

added theorem FiniteField.isPrimePow_card