Theory of monic polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
integral_normalization, which relate arbitrary polynomials to monic ones.
f : R[X] is a nonzero polynomial with root
integral_normalization f is
a monic polynomial with root
leading_coeff f * z.
integral_normalization 0 = 0.