PolynomialRing

Polynomial ring arithmetic with the generic ring tactic, over arbitrary rings

Open in Workbench View on GitHub

1-- Polynomial ring arithmetic with the generic ring tactic, over arbitrary rings.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 PolynomialRing8import Grace.Cumulus.Algebra.Polynomial.IdealSupport910section Polynomials11variable (I A add zero neg mul one : Set)12hypothesis coefficients : IsCommRing(A, add, zero, neg, mul, one)13notation ring R := (A, add, zero, neg, mul, one)14notation ring P := R[I]1516theorem square_of_sum (p q : Set)17  requires hp : p ∈ P18  requires hq : q ∈ P19  shows (p + q) * (p + q) = p * p + p * q + p * q + q * q20proof21  ring2223theorem difference_of_squares (p q : Set)24  requires hp : p ∈ P25  requires hq : q ∈ P26  shows (p + q) * (p - q) = p * p - q * q27proof28  ring2930theorem reassociate_and_cancel (p q r : Set)31  requires hp : p ∈ P32  requires hq : q ∈ P33  requires hr : r ∈ P34  shows ((p * q) * r + p) - p = p * (q * r)35proof36  ring3738theorem unit_laws (p : Set)39  requires hp : p ∈ P40  shows 1 * p + p * 0 = p41proof42  ring4344theorem monomial_support_is_an_ideal (U : Set)45  requires monomialIdeal : MonomialIdeal(I, U)46  shows IsIdeal(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), monomialIdealPolynomials(I, A, zero, U))47proof48  exact monomialIdealPolynomials.ideal with coefficients, monomialIdeal4950end Polynomials51