Repository navigation

stdlib: basic commutative algebra - #602

Open

strub wants to merge 22 commits into

mainfrom

comm-algebra

Commits on Oct 6, 2026

stdlib: basic commutative algebra
strub
committed
f7f1fea
CommAlgebra: witness-level (comax) CRT layer
strub
committed
744726e
CommAlgebra: stack as Base / Euclidean; guard dvdw
strub
committed
e0559cc
Poly: evaluation lemma library; tighten the peval definition
strub
committed
849bd69
Poly, ZModP: keep instance members as aliases; export IDPoly
strub
committed
8552b01
Poly: evaluation of polynomial products
strub
committed
d5468de
Poly: rename peval_big to peval_sum
strub
committed
0d95a1a
Poly: products of monic linear factors
strub
committed
845b893
Poly: mprod does not vanish outside its roots
strub
committed
4fa084d
Poly: simplify the monic-linear-factor lemmas
strub
committed
306c718
Poly: PolyField, polynomials over a field; Lagrange interpolation
strub
committed
00b4e51
Poly: package Lagrange interpolation in a sub-theory; tidy proofs
strub
committed
87d2303
CommAlgebra: Base owns its big operators and pushes them into Ideal
strub
committed
ac5a7aa
Ring, ZModP: delta-only mixins for IDomain and Field (pilot)
strub
committed
40e48db
Ring, ZModP: reference-bundles for domains and fields
strub
committed
db50e32
Poly: mixin architecture for the IDomain and Field levels
strub
committed
ba115dc
ZModP: remove the bundled ZModpField clone
strub
committed
3bad478
Ideal, CommAlgebra: mixin parameters; BigPoly's CR slot as alias
strub
committed
9086adf
CommAlgebra: generic congruence modulo an element (eqm)
strub
committed
a3d177a
Packed theory aliases: theory A = T1 + ... + Tn
strub
committed
76dff10
ZModP: restore the flat ZModpField namespace as a packed alias
strub
committed
0dec6fa
Proof-local reduction-opacity overrides: [-delta op] / [+delta op]
strub
committed
eb2701d

Navigation Menu

Repository navigation

stdlib: basic commutative algebra - #602

stdlib: basic commutative algebra#602
strub wants to merge 22 commits into
mainfrom
comm-algebra

Commits on Oct 6, 2026

stdlib: basic commutative algebra

CommAlgebra: witness-level (comax) CRT layer

CommAlgebra: stack as Base / Euclidean; guard dvdw

Poly: evaluation lemma library; tighten the peval definition

Poly, ZModP: keep instance members as aliases; export IDPoly

Poly: evaluation of polynomial products

Poly: rename peval_big to peval_sum

Poly: products of monic linear factors

Poly: mprod does not vanish outside its roots

Poly: simplify the monic-linear-factor lemmas

Poly: PolyField, polynomials over a field; Lagrange interpolation

Poly: package Lagrange interpolation in a sub-theory; tidy proofs

CommAlgebra: Base owns its big operators and pushes them into Ideal

Ring, ZModP: delta-only mixins for IDomain and Field (pilot)

Ring, ZModP: reference-bundles for domains and fields

Poly: mixin architecture for the IDomain and Field levels

ZModP: remove the bundled ZModpField clone

Ideal, CommAlgebra: mixin parameters; BigPoly's CR slot as alias

CommAlgebra: generic congruence modulo an element (eqm)

Packed theory aliases: theory A = T1 + ... + Tn

ZModP: restore the flat ZModpField namespace as a packed alias

Proof-local reduction-opacity overrides: [-delta op] / [+delta op]