feat: update to 4.29.1 (#207)

Author: dhsorens

README.md

@@ -75,7 +75,7 @@ import CompPoly
 
 ### Implemented highlights
 
-- **Multivariate (`CMvPolynomial`)**: full core API (`eval`, `eval₂`, `eval₂Hom`, `aeval`, `bind₁`, `rename`, `restrict*`, `finSuccEquiv`/`optionEquivLeft`, leading-term operations, `sumToIter`), plus `CommSemiring`/`CommRing`, algebra/scalar-action instances, and equivalence to Mathlib `MvPolynomial`.
+- **Multivariate (`CMvPolynomial`)**: full core API (`eval`, `eval₂`, `eval₂Hom`, `aeval`, `bind₁`, `rename`, `restrict*`, `finSuccEquiv`, leading-term operations, `sumToIter`), plus `CommSemiring`/`CommRing`, algebra/scalar-action instances, and equivalence to Mathlib `MvPolynomial`.
 - **Multilinear (`CMlPolynomial`, `CMlPolynomialEval`)**: coefficient and Boolean-hypercube evaluation representations, basis conversions, and equivalence to Mathlib's multilinear polynomial surface.
 - **Univariate (`CPolynomial`)**: full ring structure, core operations (`C`, `X`, `monomial`, `coeff`, `eval`, `eval₂`, degree/leading/support), `ringEquiv` to Mathlib `Polynomial`, and Lagrange interpolation (`basis`, `interpolate`, `interpolatePow`).
 - **Bivariate (`CBivariate`)**: specialized `CPolynomial (CPolynomial R)` API with `X`, `Y`, `monomialXY`, evaluation, leading coefficients, `swap`, and equivalence to `Polynomial (Polynomial R)`.

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8b8717467008d13b46c70040eda5b1c12d409b57",
+   "rev": "3fee686227f18dca03bb7fc42ca5a9275d6cfda6",
    "name": "ExtTreeMapLemmas",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.29.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
+   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0",
+   "inputRev": "v4.29.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -55,10 +55,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
+   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.95",
+   "inputRev": "v0.0.95+lean-v4.29.1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",

lakefile.lean

@@ -6,9 +6,9 @@ package CompPoly where
   version := v!"0.1.0"
   testDriver := "CompPolyTests"
 
-require "leanprover-community" / mathlib @ git "v4.29.0"
+require "leanprover-community" / mathlib @ git "v4.29.1"
 
-require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.29.0"
+require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.29.1"
 
 @[default_target]
 lean_lib CompPoly

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.29.1