Commit 2025-06-29 21:12 d4e3bd8e

View on Github →

chore(Complex/Polynomial): golf Irreducible.degree_le_two (over reals) (#26525)

Estimated changes

Modified Mathlib/Analysis/Complex/Polynomial/Basic.lean

modified theorem Irreducible.degree_le_two

modified theorem Irreducible.natDegree_le_two