MonicProducts
Monic products and leading coefficients over arbitrary commutative rings
1-- Monic products and leading coefficients over arbitrary commutative rings.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module MonicProductsExample7import Grace.Cumulus.Algebra.Polynomial.MonicProducts89section Polynomials10variable (I A add zero neg mul one j : Set)11notation ring R := (A, add, zero, neg, mul, one)12notation ring P := R[I]13hypothesis ring : IsCommRing(R)14hypothesis index : j ∈ I1516theorem leading (xs : List(A))17 shows polynomialLinearFactors(I, R, j, xs)(monomialShift(I, j, monomialOne(I), length{A}(xs))) = R[1]18proof19 exact polynomialLinearFactors.leading_coefficient with *2021theorem factor (a : Set) (xs : List(A))22 requires center : a ∈ R23 shows polynomialLinearFactors(I, R, j, a :: xs) =24 P[(polynomialVariable(I, R, j) - polynomialCoefficients(I, R)(a)) * polynomialLinearFactors(I, R, j, xs)]25proof26 exact polynomialLinearFactors.cons with *2728theorem nonzero (xs : List(A))29 requires nontrivial : R[1] ≠ R[0]30 shows polynomialLinearFactors(I, R, j, xs) ≠ P[0]31proof32 exact polynomialLinearFactors.nonzero with *3334-- Degree uniqueness requires nonzero leading coefficients, but no domain.35theorem degree_unique (a b : Set) (cs ds : List(A))36 requires left : a ∈ R37 requires right : b ∈ R38 requires leftNonzero : a ≠ R[0]39 requires rightNonzero : b ≠ R[0]40 requires equal : polynomialFromHorner(I, R, j, a, cs) = polynomialFromHorner(I, R, j, b, ds)41 shows length{A}(cs) = length{A}(ds)42proof43 exact polynomialFromHorner.length_unique with *4445end Polynomials4647section Extensions48variable (I A add zero neg mul one B plus z minus times unit f v j : Set)49notation ring R := (A, add, zero, neg, mul, one)50notation ring S := (B, plus, z, minus, times, unit)51hypothesis source : IsCommRing(R)52hypothesis target : IsCommRing(S)53hypothesis hom : IsRingHom(f, R, S)54hypothesis assignment : v : I → S55hypothesis index : j ∈ I5657theorem evaluate (cs : List(A))58 shows polynomialAtOver(I, R, S, f, v)(polynomialFromHorner(I, R, j, R[1], cs)) = monicValue(R, f, S, v(j), cs)59proof60 exact polynomialAtOver.from_monic_horner with *6162theorem annihilate (n : Nat) (M N w k : Set) (cs : List(A))63 requires matrixM : RingMatrix(n, R, M)64 requires matrixN : RingMatrix(n, S, N)65 requires entries : ∀ a ∈ n, ∀ b ∈ n, N[a, b] = f(M[a, b])66 requires eigenvector : LeftEigenvector(n, S, N, v(j), w)67 requires coordinate : k ∈ n68 requires representation : characteristicPolynomial(n, I, R, M, j) = polynomialFromHorner(I, R, j, R[1], cs)69 shows S[monicValue(R, f, S, v(j), cs) * w(k)] = S[0]70proof71 exact characteristicPolynomial.horner_annihilates with *7273end Extensions74