theorem Polynomial.eval_derivative_of_mem_roots {K : Type u_1} [Field K] [DecidableEq K] {f : Polynomial K} (hsplit : f.Splits) {x : K} (hx : x ∈ f.roots) : eval x (derivative f) = f.leadingCoeff * (Multiset.map (fun (x_1 : K) => x - x_1) (f.roots.erase x)).prod

Derivative of a split polynomial evaluated at one of its roots, as a product over the remaining roots: f'(x) = leadingCoeff f * ∏_{y ∈ roots.erase x} (x - y).

This is the non-monic companion of Polynomial.Splits.eval_root_derivative; it scales that monic statement by the leading coefficient. When x is a repeated root both sides vanish.

theorem Polynomial.discr_eq_prod_roots {K : Type u_1} [Field K] [DecidableEq K] {f : Polynomial K} (hf : 0 < f.degree) (hsplit : f.Splits) : f.discr = (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) * f.leadingCoeff ^ (2 * f.natDegree - 2) * (Multiset.map (fun (x : K) => (Multiset.map (fun (x_1 : K) => x - x_1) (f.roots.erase x)).prod) f.roots).prod

The root-product form of the discriminant of a split polynomial of positive degree: with n = natDegree f, discr f = (-1) ^ (n (n-1) / 2) * leadingCoeff f ^ (2 n - 2) * ∏_{x ∈ roots} ∏_{y ∈ roots.erase x} (x - y).

The double product is the off-diagonal product of root differences; it equals (-1) ^ (n(n-1)/2) * ∏_{i<j} (rᵢ - rⱼ)², so this is the classical formula.

theorem Polynomial.discr_ne_zero_of_nodup_roots {K : Type u_1} [Field K] {f : Polynomial K} (hf : 0 < f.degree) (hsplit : f.Splits) (hnd : f.roots.Nodup) : f.discr ≠ 0

The discriminant of a split polynomial of positive degree with distinct roots is nonzero.

theorem Polynomial.discr_map_of_lc {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : 0 < f.degree) (hlc : φ f.leadingCoeff ≠ 0) : (map φ f).discr = φ f.discr

Base change of the discriminant when the leading coefficient survives. The hypothesis is exactly what is needed to preserve degree and cancel the leading coefficient in Polynomial.resultant_deriv.

theorem Polynomial.discr_map_of_injective {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [IsDomain S] (φ : R →+* S) (hφ : Function.Injective ⇑φ) {f : Polynomial R} (hf : 0 < f.degree) : (map φ f).discr = φ f.discr

Base change of the discriminant along an injective ring homomorphism into a domain: discr (f.map φ) = φ (discr f), for f of positive degree. The discriminant is a universal polynomial in the coefficients, so this holds for any injective φ; the proof cancels the (nonzero) leading coefficient in the resultant identity Polynomial.resultant_deriv.

theorem Polynomial.discr_ne_zero_of_separable {K : Type u_1} [Field K] {f : Polynomial K} (hf : 0 < f.degree) (hsep : f.Separable) : f.discr ≠ 0

The discriminant of a separable polynomial of positive degree over a field is nonzero. This is the non-vanishing input Mahler's separation bound needs; it does not assume f splits (it passes to the splitting field).

theorem Polynomial.one_le_abs_discr {f : Polynomial ℤ} (hf : 0 < f.degree) (hsep : (map (Int.castRingHom ℚ) f).Separable) : 1 ≤ |f.discr|

Mahler's lower bound input: the discriminant of an integer polynomial of positive degree whose rational image is separable (equivalently squarefree over ℚ) is a nonzero integer, hence has absolute value at least 1.