Commit 2024-02-18 23:34 89162a46

View on Github →

fix: rename Irreducible.nat_degree_le_two (#10687)

Estimated changes

Modified Mathlib/Analysis/Complex/Polynomial.lean

added theorem Irreducible.natDegree_le_two

deleted theorem Irreducible.nat_degree_le_two