PolynomialEvaluation

Polynomial evaluation, using ring notation and the generic homomorphism API

Open in Workbench View on GitHub

1-- Polynomial evaluation, using ring notation and the generic homomorphism API.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 PolynomialEvaluation8import Grace.Cumulus.Algebra.Polynomial.EvaluationHom910section Evaluation11variable (I A add zero neg mul one h e : Set)12hypothesis coefficients : IsCommRing(A, add, zero, neg, mul, one)13hypothesis character : MonomialCharacter(I, A, mul, one, h)14hypothesis evaluation : e = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)15notation ring R := (A, add, zero, neg, mul, one)16notation ring P := R[I]1718theorem evaluate_product (p q : Set)19  requires hp : p ∈ P20  requires hq : q ∈ P21  shows e(P[p * q]) = R[e(p) * e(q)]22proof23  have hom := polynomialEvaluate.hom at I, A, add, zero, neg, mul, one, h with *24  rw evaluation25  exact IsRingHom.mul with hom, hp, hq2627theorem evaluate_sum (p q : Set)28  requires hp : p ∈ P29  requires hq : q ∈ P30  shows e(P[p + q]) = R[e(p) + e(q)]31proof32  have hom := polynomialEvaluate.hom at I, A, add, zero, neg, mul, one, h with *33  rw evaluation34  exact IsRingHom.add with hom, hp, hq3536theorem evaluate_constant (a : Set)37  requires ha : a ∈ R38  shows e(polynomialConstant(I, A, zero, a)) = a39proof40  rw evaluation41  exact polynomialEvaluate.constant at I, A, add, zero, neg, mul, one, h, a with *4243end Evaluation44