Mathlib Changelog
v4
Changelog
About
Github
Theorem
Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic
Modification history
2025-10-07 08:33
Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean
feat: factorization of cyclotomic polynomial over finite fields (#30032) …
Added
Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic
View on Github →