Theorem charP_of_card_eq_prime

Modification history

2025-10-07 08:33
Mathlib/Algebra/CharP/CharAndCard.lean
feat: factorization of cyclotomic polynomial over finite fields (#30032) …
Modified charP_of_card_eq_primeView on Github →
2024-06-25 09:57
Mathlib/Algebra/CharP/CharAndCard.lean
feat(Mathlib.NumberTheory.Cyclotomic.Three): add various results (#13798) …
Added charP_of_card_eq_primeView on Github →