Mathlib Changelog
v4
Changelog
About
Github
Theorem
Irreducible.degree_le_two
Modification history
2025-06-29 21:12
Mathlib/Analysis/Complex/Polynomial/Basic.lean
chore(Complex/Polynomial): golf `Irreducible.degree_le_two` (over reals) (#26525)
Modified
Irreducible.degree_le_two
View on Github →
2024-02-14 08:30
Mathlib/Analysis/Complex/Polynomial.lean
feat: an irreducible real polynomial has degree ≤2 (#10431)
Added
Irreducible.degree_le_two
View on Github →