Theorem ZMod.irreducible_of_dvd_cyclotomic_of_natDegree

Modification history

2025-10-07 08:33
Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean
feat: factorization of cyclotomic polynomial over finite fields (#30032) …
Added ZMod.irreducible_of_dvd_cyclotomic_of_natDegreeView on Github →