fix: rename Irreducible.nat_degree_le_two (#10687)

leanprover-community · Feb 18, 2024 · 89162a4 · 89162a4
1 parent b9a311a
commit 89162a4
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/Mathlib/Analysis/Complex/Polynomial.lean b/Mathlib/Analysis/Complex/Polynomial.lean
@@ -219,5 +219,8 @@ lemma Irreducible.degree_le_two {p : ℝ[X]} (hp : Irreducible p) : degree p ≤
     rwa [isUnit_iff_degree_eq_zero.1 hq, add_zero]
 
 /-- An irreducible real polynomial has natural degree at most two. -/
-lemma Irreducible.nat_degree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree p ≤ 2 :=
+lemma Irreducible.natDegree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree p ≤ 2 :=
   natDegree_le_iff_degree_le.2 hp.degree_le_two
+
+@[deprecated] -- 2024-02-18
+alias Irreducible.nat_degree_le_two := Irreducible.natDegree_le_two