Theorem Irreducible.natDegree_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.natDegree_le_twoView on Github →
2024-02-18 23:34
Mathlib/Analysis/Complex/Polynomial.lean
fix: rename Irreducible.nat_degree_le_two (#10687)
Added Irreducible.natDegree_le_twoView on Github →