Resultant lemmas

Mathlib evaluates the resultant against the linear polynomial X - C x on either side (Polynomial.resultant_X_sub_C_left, Polynomial.resultant_X_sub_C_right). This file records the companion for the reversed polynomial C x - X, which is the shape that arises as x - θ in AdjoinRoot f: the answer is f.eval x, with no sign.

The file also normalizes bounded resultants with a monic left argument. This makes the resultant independent of the chosen valid right degree bound, as needed when comparing resultant-based discriminant formulas that use different bounds.

That absence is the point. C x - X is C (-1) * (X - C x), which contributes (-1) ^ m, and resultant_X_sub_C_right contributes another (-1) ^ m, so the two cancel.

Main results

• Polynomial.resultant_C_sub_X_right
• Polynomial.Monic.resultant_of_le: for a monic left argument, the resultant is independent of the valid degree bound supplied for the right argument.

Provenance

Adapted from Michael Stoll's EllipticCurves (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, EllipticCurves/Mathlib/Basic.lean line 615, where it is a Mathlib-bound prerequisite of the explicit 2-descent.

@[simp]

theorem Polynomial.resultant_C_sub_X_right {R : Type u_1} [CommRing R] (f : Polynomial R) (x : R) (m : ℕ) (hm : f.natDegree ≤ m) : f.resultant (C x - X) m 1 = eval x f

The resultant of f with the reversed linear polynomial C x - X is f.eval x. Note the absence of a sign: C x - X is -(X - C x), and the two signs cancel.

theorem Polynomial.Monic.resultant_of_le {R : Type u_1} [CommRing R] {f g : Polynomial R} (hf : f.Monic) {n : ℕ} (hn : g.natDegree ≤ n) : f.resultant g f.natDegree n = f.resultant g

For monic f, f.resultant g does not depend on which valid upper bound is supplied for the degree of g.