Repository navigation

stdlib: basic commutative algebra - #602

Open

strub wants to merge 25 commits into

mainfrom

comm-algebra

Open

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

Commits on Oct 9, 2026
- stdlib: basic commutative algebra
  strub
  committed
  2d1245c
- CommAlgebra: witness-level (comax) CRT layer
  strub
  committed
  b590f45
- CommAlgebra: stack as Base / Euclidean; guard dvdw
  strub
  committed
  bab73a8
- Poly: evaluation lemma library; tighten the peval definition
  strub
  committed
  bf4e13c
- Poly, ZModP: keep instance members as aliases; export IDPoly
  strub
  committed
  d402332
- Poly: evaluation of polynomial products
  strub
  committed
  d315e0d
- Poly: rename peval_big to peval_sum
  strub
  committed
  bd14151
- Poly: products of monic linear factors
  strub
  committed
  4873ecc
- Poly: mprod does not vanish outside its roots
  strub
  committed
  fbce59e
- Poly: simplify the monic-linear-factor lemmas
  strub
  committed
  6621a37
- Poly: PolyField, polynomials over a field; Lagrange interpolation
  strub
  committed
  cb16aef
- Poly: package Lagrange interpolation in a sub-theory; tidy proofs
  strub
  committed
  7721f15
- CommAlgebra: Base owns its big operators and pushes them into Ideal
  strub
  committed
  8eb2004
- Ring, ZModP: delta-only mixins for IDomain and Field (pilot)
  strub
  committed
  c7a36c3
- Ring, ZModP: reference-bundles for domains and fields
  strub
  committed
  bb43761
- Poly: mixin architecture for the IDomain and Field levels
  strub
  committed
  d742de8
- ZModP: remove the bundled ZModpField clone
  strub
  committed
  d15125f
- Ideal, CommAlgebra: mixin parameters; BigPoly's CR slot as alias
  strub
  committed
  6a44cb9
- CommAlgebra: generic congruence modulo an element (eqm)
  strub
  committed
  c520c7b
- Packed theory aliases: theory A = T1 + ... + Tn
  strub
  committed
  5bcaa87
- ZModP: restore the flat ZModpField namespace as a packed alias
  strub
  committed
  fdf8356
- Proof-local reduction-opacity overrides: [-delta op] / [+delta op]
  strub
  committed
  61ffaf6
Commits on Oct 14, 2026

Navigation Menu

Repository navigation

stdlib: basic commutative algebra - #602

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

Commits on Oct 9, 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]

Commits on Oct 14, 2026

Qualified names through single-target nested theory aliases

Merge remote-tracking branch 'origin/main' into comm-algebra

Leave an alias in place of a theory cleared by a theory override