Grace/Cumulus/Algebra/Polynomial/FactorTheorem.g17

Open in Workbench Download source

Imports

Horner

Declarations

• remainder.theorem theorem derivation
• factor.theorem theorem derivation
• factor.root theorem derivation

Source

1-- The remainder and factor theorems: dividing a polynomial by X − a leaves2-- the remainder p(a), and a is a root exactly when X − a divides p3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Polynomial.FactorTheorem9import Horner1011section Rings12variable (A add zero neg mul one leading : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)15hypothesis initial : leading ∈ R1617-- The remainder theorem: p(x) = p(a) + (x − a)·q(x) with q the synthetic18-- quotient, so the remainder on division by X − a is p(a).19theorem remainder.theorem (a x c : Set) (cs : List(A))20  requires center : a ∈ R21  requires element : x ∈ R22  requires coefficient : c ∈ R23  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[hornerAt{A}(add, mul, leading, a, c :: cs) + (x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]24proof25  exact hornerAt.synthetic_division with *2627-- The factor theorem: at a root a, X − a divides p with the synthetic quotient.28theorem factor.theorem (a x c : Set) (cs : List(A))29  requires center : a ∈ R30  requires element : x ∈ R31  requires coefficient : c ∈ R32  requires root : hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]33  shows hornerAt{A}(add, mul, leading, x, c :: cs) = R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]34proof35  have division := hornerAt.synthetic_division at A, add, zero, neg, mul, one, leading, a, x, c, cs with *36  have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, cs with *37  have quotientValue := hornerAt.closed at A, add, zero, neg, mul, one, leading, x, hornerQuotient{A}(add, mul, leading, a, cs) with *38  rw root at division39  rw division40  ring4142-- Conversely, a factor X − a forces a root at a.43theorem factor.root (a c : Set) (cs : List(A))44  requires center : a ∈ R45  requires coefficient : c ∈ R46  requires factor : ∀ x ∈ R, hornerAt{A}(add, mul, leading, x, c :: cs) = R[(x - a) * hornerAt{A}(add, mul, leading, x, hornerQuotient{A}(add, mul, leading, a, cs))]47  shows hornerAt{A}(add, mul, leading, a, c :: cs) = R[0]48proof49  have quotient := hornerQuotient.closed at A, add, zero, neg, mul, one, leading, a, cs with *50  have quotientValue := hornerAt.closed at A, add, zero, neg, mul, one, leading, a, hornerQuotient{A}(add, mul, leading, a, cs) with *51  have atRoot := factor with center52  rw atRoot53  ring5455end Rings56