Commit 2025-05-27 08:30 cf30ea73

feat(Polynomial.FieldDivision): Several lemmas about normalized polynomials over a field (#25149) We prove the following lemmas (over a field):

• A polynomial is normalized iff it is monic
• p is in normalizedFactors q iff p is irreducible, monic and divides q
• normalize commutes with polynomial map of ring homo (between fields)