EmptyVariablePolynomials

Eliminating zero-variable polynomial coefficients from algebraic relations (ZF)

Open in Workbench View on GitHub

1-- Eliminating zero-variable polynomial coefficients from algebraic relations (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 EmptyVariablePolynomials8import Grace.Cumulus.Algebra.Polynomial.EmptyVariables910theorem every_polynomial_is_constant (A zero p : Set)11  requires zeroIn : zero ∈ A12  requires polynomial : p ∈ polynomials(∅, A, zero)13  shows p = polynomialConstant(∅, A, zero, emptyPolynomialCoefficient(A, zero)(p))14proof15  exact polynomial.empty_constant with *1617theorem nonzero_coefficient (A zero p : Set)18  requires zeroIn : zero ∈ A19  requires polynomial : p ∈ polynomials(∅, A, zero)20  requires nonzero : p ≠ constantFunction(monomials(∅), A, zero)21  shows emptyPolynomialCoefficient(A, zero)(p) ≠ zero22proof23  exact emptyPolynomialCoefficient.nonzero with *2425section Algebras26variable (A add zero neg mul one B plus z minus times unit f v x : Set)27notation ring R := (A, add, zero, neg, mul, one)28notation ring S := (B, plus, z, minus, times, unit)29notation ring Q := R[∅]30hypothesis source : IsCommRing(R)31hypothesis target : IsCommRing(S)32hypothesis hom : IsRingHom(f, R, S)33hypothesis assignment : v : ∅ → S3435theorem evaluation_is_coefficient_evaluation (p : Set)36  requires polynomial : p ∈ Q37  shows polynomialAtOver(∅, R, S, f, v)(p) = f(emptyPolynomialCoefficient(A, zero)(p))38proof39  exact polynomialAtOver.empty_value with *4041theorem transport_algebraicity42  requires algebraic : AlgebraicOver(polynomialAtOver(∅, R, S, f, v), Q, S, x)43  shows AlgebraicOver(f, R, S, x)44proof45  exact AlgebraicOver.empty_variables with *4647end Algebras48