Theorem CharP.prime_ringChar

Modification history

2025-01-20 15:19
Mathlib/Algebra/CharP/Lemmas.lean
chore(Algebra/CharP): `prime_ringChar` and `isPrimePow_card` (#20860) …
Added CharP.prime_ringCharView on Github →