PolynomialStarter
Monomial arithmetic and the polynomial coefficient carrier
1-- Monomial arithmetic and the polynomial coefficient carrier.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialStarter8import Grace.Cumulus.Algebra.Polynomial910theorem monomial_structure (I : Set)11 shows IsCommMonoid(monomials(I), monomialMul(I), monomialOne(I))12proof13 exact monomials.comm_monoid1415theorem squared_variable (I j : Set)16 requires index : j ∈ I17 shows monomialProduct(I, monomialVariable(I, j), monomialVariable(I, j))(j) = 218proof19 have variable := monomialVariable.member at I, j20 have product := monomialProduct.value at I, monomialVariable(I, j), monomialVariable(I, j), j with *21 have exponent := monomialVariable.same with index22 rw product23 rw exponent24 compute2526theorem faithful_constants (I A z a b : Set)27 requires zeroIn : z ∈ A28 requires left : a ∈ A29 requires right : b ∈ A30 requires equal : polynomialConstant(I, A, z, a) = polynomialConstant(I, A, z, b)31 shows a = b32proof33 exact polynomialConstant.injective at I, A, z, a, b with *3435theorem faithful_variables (I A z unit j k : Set)36 requires zeroIn : z ∈ A37 requires unitIn : unit ∈ A38 requires nonzero : unit ≠ z39 requires first : j ∈ I40 requires second : k ∈ I41 requires equal : polynomialVariable(I, A, z, unit, j) = polynomialVariable(I, A, z, unit, k)42 shows j = k43proof44 exact polynomialVariable.injective at I, A, z, unit, j, k with *4546theorem ignore_new_zero_term (V A add zero neg mul one w a : Set)47 requires ring : IsCommRing(A, add, zero, neg, mul, one)48 requires finite : Finite(V)49 requires weights : w : insert(a, V) → A50 requires fresh : ¬(a ∈ V)51 requires vanishes : w(a) = zero52 shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one, w) =53 finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V))54proof55 exact finiteRingSum.insert_zero at V, A, add, zero, neg, mul, one, w, a with *56