Theorem Polynomial.irreducible_of_degree_le_three_of_not_isRoot

Modification history

2025-04-11 13:00
Mathlib/Algebra/Polynomial/SpecificDegree.lean
feat(RingTheory/Polynomial/Eisenstein/Generalized): a generalized version of the Eisenstein criterion (#23710) …
Added Polynomial.irreducible_of_degree_le_three_of_not_isRootView on Github →