Theorem Irreducible.degree_pos

Modification history

2025-08-22 22:36
Mathlib/Algebra/Polynomial/FieldDivision.lean
feat: irreducible polynomial has positive degree (#28587)
Added Irreducible.degree_posView on Github →