Remainders by constant multiples, and the quotient by X - x at x

Candidates for Mathlib.Algebra.Polynomial.FieldDivision: over a commutative ring, the quotient of p by X - x takes the value p'(x) at x (Polynomial.eval_divByMonic_X_sub_C); over a field, a constant factor of the dividend comes out of the remainder (Polynomial.C_mul_mod, from Polynomial.smul_modByMonic), and a nonzero constant factor of the divisor does not change it (Polynomial.mod_C_mul, from Polynomial.div_C_mul).

theorem Polynomial.eval_divByMonic_X_sub_C {R : Type u_1} [CommRing R] (p : Polynomial R) (x : R) : eval x (p /ₘ (X - C x)) = eval x (derivative p)

The quotient of p by X - x takes the value p'(x) at x, so that at a root x of p, p = (X - x) q with q(x) = p'(x).

theorem Polynomial.C_mul_mod {K : Type u_1} [Field K] (c : K) (p q : Polynomial K) : C c * p % q = C c * (p % q)

A constant factor of the dividend comes out of the remainder.

theorem Polynomial.mod_C_mul {K : Type u_1} [Field K] {c : K} (hc : c ≠ 0) (p q : Polynomial K) : p % (C c * q) = p % q

A nonzero constant factor of the divisor does not change the remainder.