mathlib documentation

data.polynomial.integral_normalization

Theory of monic polynomials

We define integral_normalization, which relate arbitrary polynomials to monic ones.

If f : polynomial R is a nonzero polynomial with root z, integral_normalization f is a monic polynomial with root leading_coeff f * z.

Moreover, integral_normalization 0 = 0.

Equations
theorem polynomial.integral_normalization_eval₂_eq_zero {R : Type u} {S : Type v} [integral_domain R] [comm_ring S] {p : polynomial R} (hp : p 0) (f : R →+* S) {z : S} :
polynomial.eval₂ f z p = 0(∀ (x : R), f x = 0x = 0)polynomial.eval₂ f (z * f p.leading_coeff) p.integral_normalization = 0

theorem polynomial.integral_normalization_aeval_eq_zero {R : Type u} {S : Type v} [integral_domain R] [comm_ring S] [algebra R S] {f : polynomial R} (hf : f 0) {z : S} :
(polynomial.aeval z) f = 0(∀ (x : R), (algebra_map R S) x = 0x = 0)(polynomial.aeval (z * (algebra_map R S) f.leading_coeff)) f.integral_normalization = 0