The linear factor X - C x, and its reverse

Linear factors, scalar factorizations, and the full power of a root factor. Over an ordered field, a polynomial of degree at most one has constant sign on a root-free interval.

The reversed factor C x - X — the shape that arises as x - θ in AdjoinRoot f — has degree 1, like X - C x itself, which is the form Mathlib states.

A polynomial of degree at most one with root x is C γ * (X - C x) for a single scalar γ. Writing it as C a * X + C b, the root condition gives a * x + b = 0, which identifies the constant term and factors the polynomial. This works over noncommutative rings, with the scalar factor on the left.

Factoring out the full multiplicity of a root of a nonzero polynomial leaves a cofactor that does not vanish at the root.

Main results

• Polynomial.natDegree_C_sub_X: the reversed linear factor C x - X has degree 1.
• Polynomial.exists_eq_C_mul_X_sub_C_of_natDegree_le_one: a polynomial of natDegree ≤ 1 with root x is C γ * (X - C x) for some γ.
• Polynomial.eval_mul_pos_of_natDegree_le_one_of_no_roots: constant nonzero sign on a root-free closed interval for polynomials of degree at most one.
• Polynomial.derivative_root_factors: factor the derivative of a polynomial with two root powers.
• Polynomial.IsRoot.exists_eq_pow_succ_mul: factor out a positive power of X - C x, leaving a cofactor nonzero at x.
• Polynomial.rootMultiplicity_add_eq_left_of_dvd: adding a multiple of a higher power of X - C x leaves the root multiplicity at x unchanged.

Provenance

The statement of exists_eq_C_mul_X_sub_C_of_natDegree_le_one generalizes the commutative-ring result adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, revision 66889eada51a), EllipticCurves/Mathlib/Basic.lean. Its consumer is the x - T descent map of TauCeti/AlgebraicGeometry/EllipticCurve/MordellWeil/XSubT.lean, where it pins down the line through a 2-torsion point.

@[simp]

theorem Polynomial.natDegree_C_sub_X {R : Type u_2} [Ring R] [Nontrivial R] (x : R) : (C x - X).natDegree = 1

The reversed linear polynomial C x - X has degree 1, like X - C x.

theorem Polynomial.exists_eq_C_mul_X_sub_C_of_natDegree_le_one {R : Type u_1} [Ring R] {p : Polynomial R} (hdeg : p.natDegree ≤ 1) {x : R} (hx : p.IsRoot x) : ∃ (γ : R), p = C γ * (X - C x)

A polynomial of degree at most one with prescribed root x is a left scalar multiple of X - C x, over any ring.

theorem Polynomial.IsRoot.exists_eq_pow_succ_mul {A : Type u_2} [CommRing A] {p : Polynomial A} {a : A} (ha : p.IsRoot a) (hp : p ≠ 0) : ∃ (m : ℕ) (q : Polynomial A), p = (X - C a) ^ (m + 1) * q ∧ eval a q ≠ 0

A root of a nonzero polynomial factors out with positive multiplicity and a cofactor that does not vanish at the root.

theorem Polynomial.rootMultiplicity_add_eq_left_of_dvd {A : Type u_2} [Ring A] {p q : Polynomial A} {a : A} (hp : p ≠ 0) (hq : (X - C a) ^ (rootMultiplicity a p + 1) ∣ q) : rootMultiplicity a (p + q) = rootMultiplicity a p

Adding a multiple of a higher power of X - C a does not change the root multiplicity at a of a nonzero polynomial.

theorem Polynomial.eval_mul_pos_of_natDegree_le_one_of_no_roots {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p : Polynomial R} (hdeg : p.natDegree ≤ 1) {a b : R} (hab : a ≤ b) (hroot : ∀ x ∈ Set.Icc a b, eval x p ≠ 0) : 0 < eval a p * eval b p

A polynomial of degree at most one has constant nonzero sign on an interval without a root.

theorem Polynomial.derivative_root_factors {A : Type u_2} [CommRing A] (a b : A) (m n : ℕ) (r : Polynomial A) : derivative ((X - C a) ^ (m + 1) * ((X - C b) ^ (n + 1) * r)) = (X - C a) ^ m * (X - C b) ^ n * (C (↑m + 1) * (X - C b) * r + C (↑n + 1) * (X - C a) * r + (X - C a) * (X - C b) * derivative r)

Factor the derivative after removing the powers contributed by two roots.