Degree of a normalized polynomial

Over a domain R with a NormalizationMonoid, normalize p is p times a unit, so it has the same degree as p. Mathlib states this (Polynomial.degree_normalize, Polynomial.natDegree_normalize) only over a field; here it is proved for any such domain, for instance for ℤ[X].

@[simp]

theorem Polynomial.degree_normalize' {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] (p : Polynomial R) : (normalize p).degree = p.degree

Normalizing a polynomial over a domain preserves its degree. This generalizes Mathlib's Polynomial.degree_normalize from fields to any domain with a NormalizationMonoid.

@[simp]

theorem Polynomial.natDegree_normalize' {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] (p : Polynomial R) : (normalize p).natDegree = p.natDegree

Normalizing a polynomial over a domain preserves its natural degree. This generalizes Mathlib's Polynomial.natDegree_normalize from fields to any domain with a NormalizationMonoid.