PolynomialRoots

Finite roots and nonvanishing of coefficient-list polynomials, in ZF

Open in Workbench View on GitHub

1-- Finite roots and nonvanishing of coefficient-list polynomials, in ZF.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialRoots8import Grace.Cumulus.Algebra.Polynomial.HornerRoots910section Fields11variable (A add z neg mul one leading : Set)12notation ring R := (A, add, z, neg, mul, one)13hypothesis field : IsField(R)14hypothesis initial : leading ∈ R15hypothesis nonzero : leading ≠ R[0]1617theorem finitely_many_roots (cs : List(A))18  shows Finite(hornerRoots{A}(add, z, mul, leading, cs))19proof20  exact hornerRoots.finite with *2122theorem nonvanishing (cs : List(A))23  requires infinite : ¬Finite(R)24  shows ∃ x ∈ R, hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]25proof26  exact hornerAt.exists_nonzero with *2728theorem nonvanishing_outside_finite_set (F : Set) (cs : List(A))29  requires infinite : ¬Finite(R)30  requires excluded : Finite(F)31  shows ∃ x ∈ R, ¬(x ∈ F) ∧ hornerAt{A}(add, mul, leading, x, cs) ≠ R[0]32proof33  exact hornerAt.exists_nonzero_avoiding with *3435end Fields36