stdlib: basic commutative algebra - #602

Open

strub wants to merge 23 commits into

mainfrom

Commits on Jul 17, 2026

stdlib: basic commutative algebra
strub
committed
4022832
CommAlgebra: witness-level (comax) CRT layer
strub
committed
7ad5f04
CommAlgebra: stack as Base / Euclidean; guard dvdw
strub
committed
2d510c3
Poly: evaluation lemma library; tighten the peval definition
strub
committed
d1603dc
Poly, ZModP: keep instance members as aliases; export IDPoly
strub
committed
1696643
Poly: evaluation of polynomial products
strub
committed
fdd2dcb
Poly: rename peval_big to peval_sum
strub
committed
bfd7ee8
Poly: products of monic linear factors
strub
committed
f3fbf4e
Poly: mprod does not vanish outside its roots
strub
committed
d263dec
Poly: simplify the monic-linear-factor lemmas
strub
committed
3c6febe
Poly: PolyField, polynomials over a field; Lagrange interpolation
strub
committed
9b347d0
Poly: package Lagrange interpolation in a sub-theory; tidy proofs
strub
committed
b55d7a6
CommAlgebra: Base owns its big operators and pushes them into Ideal
strub
committed
4d3f588

Commits on Jul 18, 2026

Ring, ZModP: delta-only mixins for IDomain and Field (pilot)
strub
committed
bbb6cb1
Ring, ZModP: reference-bundles for domains and fields
strub
committed
e6b9ba1
Poly: mixin architecture for the IDomain and Field levels
strub
committed
93e2b90
ZModP: remove the bundled ZModpField clone
strub
committed
538159e
Ideal, CommAlgebra: mixin parameters; BigPoly's CR slot as alias
strub
committed
5734cf6
CommAlgebra: generic congruence modulo an element (eqm)
strub
committed
95b5855

Commits on Jul 19, 2026

Packed theory aliases: theory A = T1 + ... + Tn
strub
committed
1c08319
ZModP: restore the flat ZModpField namespace as a packed alias
strub
committed
7ae031c

Commits on Jul 21, 2026