Theorem Irreducible.natDegree_pos

Modification history

2025-08-22 22:36
Mathlib/Algebra/Polynomial/FieldDivision.lean
feat: irreducible polynomial has positive degree (#28587)
Modified Irreducible.natDegree_posView on Github →
2025-04-10 13:15
Mathlib/Algebra/Polynomial/FieldDivision.lean
feat: generalize Mathlib.Algebra.Order + Polynomial (#23153) …
Modified Irreducible.natDegree_posView on Github →
2024-02-15 16:16
Mathlib/Data/Polynomial/FieldDivision.lean
feat: add some simple results regarding polynomials (#10572) …
Added Irreducible.natDegree_posView on Github →