Commit 2024-10-23 10:42 9389838e
View on Github →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.