chore(Algebra/Polynomial): normalize_monic as alias for Monic.normalize_eq_self (#18024)

Discovered in #18006.

As far as I can tell, neither lemma actually is used anywhere in Mathlib, so I arbitrarily picked the unnamespaced one to be a deprecated alias for the other. Please feel free to bikeshed over which one should win.

Author: Vierkantor

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -202,6 +202,9 @@ theorem Monic.normalize_eq_self {p : R[X]} (hp : p.Monic) : normalize p = p := b
   simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
     Units.val_one, Polynomial.C.map_one, mul_one]
 
+@[deprecated Polynomial.Monic.normalize_eq_self (since := "2024-10-21")]
+alias normalize_monic := Monic.normalize_eq_self
+
 theorem roots_normalize {p : R[X]} : (normalize p).roots = p.roots := by
   rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]
 
@@ -524,8 +527,6 @@ theorem coe_normUnit_of_ne_zero [DecidableEq R] (hp : p ≠ 0) :
   have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp
   simp [CommGroupWithZero.coe_normUnit _ this]
 
-theorem normalize_monic [DecidableEq R] (h : Monic p) : normalize p = p := by simp [h]
-
 theorem map_dvd_map' [Field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y := by
   by_cases H : x = 0
   · rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero]