refactor(comp-poly): canonicalize polynomial APIs and tighten assumptions by quangvdao · Pull Request #154 · Verified-zkEVM/CompPoly

quangvdao · 2026-03-12T01:38:24Z

Summary

Stabilize the computable polynomial representations around semantic canonicality, remove the native_decide regressions, and restore the affected computable bridge and bounded-degree APIs in a kernel-safe way.
Minimize typeclass assumptions across the univariate raw/canonical layers, quotient model, univariate and bivariate toPoly bridges, and selected multivariate/multilinear helpers by removing blanket section scopes and pushing assumptions down onto individual declarations.
Add regression tests and agent/wiki guidance so future changes keep the same minimal-assumption discipline.

Key Changes

Area	Change
Canonical carriers	Introduce and propagate semantic canonicality for `CPolynomial` and `CBivariate`, update raw/core canonicality lemmas, and make the canonical carriers more instance-stable.
Kernel-safe computability	Remove `native_decide` from the affected pathway and rebuild the relevant `degreeLT` / `toPoly` pieces so they remain computable and kernel-checked.
Univariate API tightening	Sweep `CompPoly/Univariate/Raw/Core.lean`, `Raw/Ops.lean`, `Raw/Proofs.lean`, `Basic.lean`, and `Linear.lean` to remove blanket `variable` declarations and give each definition, instance, and theorem only the assumptions it actually uses.
Quotient model	Generalize `CompPoly/Univariate/Quotient.lean` and `QuotientEquiv.lean`, including lowering the quotient carrier to `Zero`, pushing add/mul/pow to the weaker algebraic boundary, and tightening the quotient-to-`Polynomial` bridge.
Univariate bridges	Lower `CompPoly/Univariate/ToPoly/Core.lean`, `ToPoly/Degree.lean`, and `ToPoly/Equiv.lean` to semiring-level assumptions where possible, while keeping genuinely subtractive facts explicitly ring-scoped.
Bivariate bridges	Tighten `CompPoly/Bivariate/Basic.lean` and `Bivariate/ToPoly.lean`, including semiring-level transport lemmas for coefficients, supports, degrees, evaluation, swap, and leading-coefficient results.
Multivariate / multilinear	Lower selected core helper definitions in `CompPoly/Multivariate/{Operations,Lawful,CMvPolynomial,MvPolyEquiv/Instances}.lean` and `CompPoly/Multilinear/{Basic,Equiv}.lean`, while preserving inference behavior for mixed-arity fallback instances.
Docs and tests	Add `docs/wiki/typeclass-minimization.md`, link it from `AGENTS.md` and the wiki index, and add/update regression coverage in `tests/CompPolyTests.lean`, `tests/CompPolyTests/Bivariate/Basic.lean`, and `tests/CompPolyTests/Univariate/Linear.lean`.

Testing

lake build CompPolyTests
python3 scripts/lint-style.py CompPoly/Univariate/Raw/Core.lean CompPoly/Univariate/Raw/Ops.lean CompPoly/Univariate/Raw/Proofs.lean CompPoly/Univariate/Raw/Division.lean CompPoly/Univariate/Basic.lean CompPoly/Univariate/Linear.lean CompPoly/Univariate/Quotient.lean CompPoly/Univariate/QuotientEquiv.lean CompPoly/Univariate/ToPoly/Core.lean CompPoly/Univariate/ToPoly/Degree.lean CompPoly/Univariate/ToPoly/Equiv.lean CompPoly/Bivariate/ToPoly.lean CompPoly/Multivariate/Lawful.lean CompPoly/Multilinear/Basic.lean
python3 ./scripts/check-docs-integrity.py
GitHub Actions: Lean Action CI, Lint Style, Docs Integrity, PR Review, and PR Summary

Review Guidance

Focus on:

The semantic-canonicality transition and the kernel-safe replacements for the removed native_decide path.
The declaration-by-declaration typeclass weakening across univariate core APIs, quotient/bridge layers, and the bivariate transport lemmas.
The mixed-arity multivariate fallback instances, which were intentionally kept low-priority to avoid interfering with same-arity inference.
The new repo guidance in docs/wiki/typeclass-minimization.md, which documents the minimal-typeclass discipline used throughout this refactor.

Switch the computable polynomial carriers to semantic canonicality so they no longer depend on a particular `BEq`, and rebuild the bounded-degree transport directly so it stays computable. Add kernel-safe regression coverage for the updated univariate and bivariate APIs. Made-with: Cursor

github-actions · 2026-03-12T01:39:14Z

Build Timing Report

Commit: c4ed287
Message: Merge ed366b0 into 92eb159
Ref: quang/cpoly-refactor
Comparison baseline: 92eb159 from merge-base on master.
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	224.22	256.41	+32.19	ok
Warm rebuild	1.61	1.76	+0.15	ok
Test path	9.23	12.83	+3.60	ok

Incremental Rebuild Signal

Warm rebuild saved 254.65s vs clean (145.69x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
85.00	84.00	+1.00	`CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean`
52.00	45.00	+7.00	`CompPoly/Fields/Binary/Tower/Abstract/Basis.lean`
49.00	43.00	+6.00	`CompPoly/Bivariate/ToPoly.lean`
33.00	25.00	+8.00	`CompPoly/Fields/Binary/BF128Ghash/Impl.lean`
29.00	25.00	+4.00	`CompPoly/Univariate/Raw/Proofs.lean`
23.00	21.00	+2.00	`CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean`
23.00	19.00	+4.00	`CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean`
22.00	18.00	+4.00	`CompPoly/Univariate/Lagrange.lean`
19.00	17.00	+2.00	`CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean`
16.00	14.00	+2.00	`CompPoly/Fields/Binary/AdditiveNTT/Domain.lean`
16.00	14.00	+2.00	`CompPoly/Univariate/Basic.lean`
16.00	14.00	+2.00	`CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean`
16.00	11.00	+5.00	`CompPoly/Multivariate/Unlawful.lean`
15.00	13.00	+2.00	`CompPoly/Fields/Binary/Tower/Abstract/Core.lean`
13.00	13.00	+0.00	`CompPoly/Univariate/Quotient.lean`
12.00	10.00	+2.00	`CompPoly/Fields/KoalaBear.lean`
11.00	9.20	+1.80	`CompPoly/Data/Nat/Bitwise.lean`
11.00	9.40	+1.60	`CompPoly/Fields/Basic.lean`
11.00	3.80	+7.20	`CompPoly/Fields/BN254.lean`
11.00	8.80	+2.20	`CompPoly/Multilinear/Basic.lean`

github-actions · 2026-03-12T01:41:23Z

🤖 Gemini PR Summary

Mathematical Refactoring and Generalization

Semantic Canonicality: Transitions CPolynomial and CBivariate to a model tracking canonicity via an IsCanonical predicate (ensuring no trailing zeros). This enables core operations like coeff, degree, and size to function with minimal requirements such as Zero or BEq instead of full Semiring structures.
Typeclass Tightening: Enforces a library-wide "minimal assumption" policy. Blanket variable blocks are removed in favor of declaration-specific assumptions across univariate core APIs, quotient layers, and bivariate transport lemmas.
Algebraic Generalization:
- Lowers multivariate and multilinear operations from CommRing to CommSemiring or basic Zero/Add structures.
- Generalizes CompPoly/Univariate/Quotient.lean and QuotientEquiv.lean by lowering the quotient carrier to Zero and pushing Add/Mul/Pow to weaker algebraic boundaries.
Bounded Degree Representation: Refactors degreeLE and degreeLT to use internal degreeBound properties, allowing for direct AddCommMonoid and Module instances in a computable manner.

Computability and Kernel Stability

Kernel-Safe Pathways: Removes native_decide from the computation pipeline.
Bridge Optimization: Rebuilds toPoly bridges and degree-bound checks to be fully kernel-checked, ensuring polynomial conversions and properties remain checkable without external dependencies.
Bivariate Transport: Tightens CompPoly/Bivariate/ToPoly.lean to provide semiring-level transport lemmas for coefficients, supports, degrees, evaluation, and leading coefficients.

Documentation and Infrastructure

Minimization Policy: Introduces docs/wiki/typeclass-minimization.md and updates AGENTS.md to formalize the discipline of using the weakest possible mathematical assumptions.
Regression Testing: Adds test suites in tests/CompPolyTests/ for univariate, bivariate, and linear modules to ensure instance stability and prevent typeclass inference regressions.

Status on Proof Completion:

No new sorry or admit placeholders were introduced in this PR. All proofs have been refactored to align with the weakened typeclass constraints.

Statistics

Metric	Count
📝 Files Changed	25
✅ Lines Added	1422
❌ Lines Removed	892

Lean Declarations

✏️ **Removed:** 12 declaration(s)

theorem degreeLE_map_toPolyLinearEquiv {n : WithBot ℕ} : in CompPoly/Univariate/ToPoly/Degree.lean
lemma toPolyLinearEquiv_X_pow [Nontrivial R] (k : ℕ) : in CompPoly/Univariate/ToPoly/Degree.lean
lemma degreeLTEquiv_map_add (n : ℕ) in CompPoly/Univariate/Linear.lean
theorem degreeLT_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} : in CompPoly/Univariate/ToPoly/Degree.lean
instance [CommRing R] [BEq R] [LawfulBEq R] : CommRing (QuotientCPolynomial R) where in CompPoly/Univariate/Quotient.lean
instance [Nontrivial R] : CommRing (CPolynomial R) where in CompPoly/Univariate/Basic.lean
instance [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
theorem degreeLT_map_toPolyLinearEquiv {n : ℕ} : in CompPoly/Univariate/ToPoly/Degree.lean
instance [LawfulBEq R] : Ring (QuotientCPolynomial R) where in CompPoly/Univariate/Quotient.lean
theorem degreeLE_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} : in CompPoly/Univariate/ToPoly/Degree.lean
lemma degreeLTEquiv_map_smul (n : ℕ) in CompPoly/Univariate/Linear.lean
def degreeLTEquiv (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] [DecidableEq S] (n : ℕ) : in CompPoly/Univariate/Linear.lean

✏️ **Added:** 35 declaration(s)

instance [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommRing (CPolynomial R) where in CompPoly/Univariate/Basic.lean
instance [Neg R] : Neg (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean
theorem isCanonical_empty [Zero R] : IsCanonical (mk (R in CompPoly/Univariate/Raw/Core.lean
instance [IntCast R] : IntCast (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean
instance [NatCast R] : NatCast (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean
theorem mem_degreeLT_iff_size_le {n : ℕ} {p : CPolynomial R} : in CompPoly/Univariate/Linear.lean
instance [Zero R] : Inhabited (CPolynomial R) in CompPoly/Univariate/Basic.lean
instance [Zero R] [Add R] [Neg R] [BEq R] : Sub (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean
def degreeLTCoeffs (n : ℕ) : ↥(degreeLT (R in CompPoly/Univariate/Linear.lean
theorem isCanonical_of_trim_eq [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean
def IsCanonical [Zero R] (p : CPolynomial.Raw R) : Prop in CompPoly/Univariate/Raw/Core.lean
theorem trim_eq_of_isCanonical [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean
theorem smul_mem_degreeLT {n : ℕ} (r : R) {p : CPolynomial R} in CompPoly/Univariate/Linear.lean
instance [Ring R] [BEq R] [LawfulBEq R] : Sub (QuotientCPolynomial R) in CompPoly/Univariate/Quotient.lean
abbrev degreeLTLinearEquiv [DecidableEq R] (n : ℕ) : in CompPoly/Univariate/ToPoly/Degree.lean
instance [One R] : One (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean
instance [NegZeroClass R] : Neg (QuotientCPolynomial R) in CompPoly/Univariate/Quotient.lean
def degreeLTEquiv [DecidableEq R] (n : ℕ) : in CompPoly/Univariate/ToPoly/Degree.lean
theorem nsmul_mem_degreeLT {n m : ℕ} {p : CPolynomial R} in CompPoly/Univariate/Linear.lean
instance [Semiring R] [BEq R] : Pow (CPolynomial.Raw R) Nat in CompPoly/Univariate/Raw/Ops.lean
theorem isCanonical_trim [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean
theorem isCanonical_ext [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial.Raw R} in CompPoly/Univariate/Raw/Core.lean
theorem isCanonical_toImpl (p : R[X]) : CPolynomial.Raw.IsCanonical p.toImpl in CompPoly/Univariate/ToPoly/Core.lean
theorem zero_mem_degreeLT (n : ℕ) : (0 : CPolynomial R) ∈ degreeLT (R in CompPoly/Univariate/Linear.lean
instance [Mul R] : SMul R (CPolynomial.Raw R) in CompPoly/Univariate/Raw/Ops.lean
theorem add_mem_degreeLT {n : ℕ} {p q : CPolynomial R} in CompPoly/Univariate/Linear.lean
instance [Neg R] : Neg (Lawful n R) in CompPoly/Multivariate/Lawful.lean
lemma monomial_mem_degreeLT [DecidableEq R] {n : ℕ} (i : Fin n) (c : R) : in CompPoly/Univariate/ToPoly/Degree.lean
instance [Field R] [BEq R] [LawfulBEq R] : Mod (CPolynomial R) in CompPoly/Univariate/Basic.lean
instance [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R) where in CompPoly/Univariate/Basic.lean
instance [Add R] [Neg R] : Sub (Lawful n R) in CompPoly/Multivariate/Lawful.lean
instance [Zero R] [IntCast R] : IntCast (QuotientCPolynomial R) in CompPoly/Univariate/Quotient.lean
theorem isCanonical_of_size_zero [Zero R] {p : CPolynomial.Raw R} (hp : p.size = 0) : in CompPoly/Univariate/Raw/Core.lean
instance [DecidableEq R] : DecidableEq (CBivariate R) in CompPoly/Bivariate/Basic.lean
instance [BEq R] [LawfulBEq R] : LawfulBEq (CBivariate R) in CompPoly/Bivariate/Basic.lean

✏️ **Affected:** 280 declaration(s) (line number changed)

lemma coeff_mul [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L230 to L267
def mulDescending [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L373 to L379
lemma add_comm : ∀ (a b : QuotientCPolynomial R), a + b = b + a in CompPoly/Univariate/Quotient.lean moved from L478 to L492
lemma Raw.toPoly_X {R : Type*} [Semiring R] : in CompPoly/Univariate/ToPoly/Equiv.lean moved from L109 to L107
def nsmulDescending [Semiring R] [BEq R] (n : ℕ) (p : CPolynomial.Raw R) : QuotientCPolynomial R in CompPoly/Univariate/Quotient.lean moved from L286 to L288
lemma coeff_X [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i : ℕ) : in CompPoly/Univariate/Basic.lean moved from L204 to L239
def degreeLT (n : ℕ) : Set (CPolynomial R) in CompPoly/Univariate/Linear.lean moved from L36 to L41
def QuotientCPolynomial (R : Type*) [Zero R] in CompPoly/Univariate/Quotient.lean moved from L61 to L61
def monic [Zero R] [One R] [BEq R] (p : CPolynomial.Raw R) : Bool in CompPoly/Univariate/Raw/Ops.lean moved from L116 to L115
def degreeBound [Zero R] (p : CPolynomial R) : WithBot Nat in CompPoly/Univariate/Basic.lean moved from L184 to L217
lemma coeff_C [Zero R] [BEq R] [LawfulBEq R] (r : R) (i : ℕ) : in CompPoly/Univariate/Basic.lean moved from L198 to L231
theorem coeff_mul_X_succ [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L351 to L402
def eval₂ [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial.Raw R) : S in CompPoly/Univariate/Raw/Ops.lean moved from L35 to L32
lemma degree_eq_support_max_aux_mem_support [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L524 to L590
lemma coeff_eq_getElem [Zero Q] {p : CPolynomial.Raw Q} {i} (hp : i < p.size) : in CompPoly/Univariate/Raw/Core.lean moved from L268 to L277
instance instEquivalenceEquiv [Zero R] : Equivalence (equiv (R in CompPoly/Univariate/Quotient.lean moved from L47 to L47
lemma neg_coeff {R : Type*} [NegZeroClass R] (p : CPolynomial.Raw R) (i : ℕ) : in CompPoly/Univariate/Raw/Proofs.lean moved from L945 to L940
theorem size_eq_degree_plus_one [Zero R] [BEq R] in CompPoly/Univariate/Raw/Core.lean moved from L210 to L214
theorem add_zero [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p + 0 = p in CompPoly/Univariate/Basic.lean moved from L89 to L104
theorem neg_add_cancel [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : -p + p = 0 in CompPoly/Univariate/Basic.lean moved from L846 to L900
def eval [Semiring R] (x : R) (p : CPolynomial.Raw R) : R in CompPoly/Univariate/Raw/Ops.lean moved from L40 to L37
theorem support_empty_iff [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : in CompPoly/Univariate/Basic.lean moved from L268 to L309
def evalEval {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Bivariate/Basic.lean moved from L160 to L177
lemma toPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L102 to L102
def addDescending [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L244 to L245
theorem canonical_iff [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} : in CompPoly/Univariate/Raw/Core.lean moved from L399 to L414
lemma mul_descends [Semiring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L376 to L383
def degree [Zero R] [BEq R] (p : CPolynomial.Raw R) : WithBot ℕ in CompPoly/Univariate/Raw/Core.lean moved from L80 to L77
def monomial [Zero R] [DecidableEq R] (n : ℕ) (c : R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Core.lean moved from L65 to L62
def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L52 to L52
lemma Raw.toPoly_one {R : Type*} [Semiring R] : in CompPoly/Univariate/ToPoly/Equiv.lean moved from L91 to L90
lemma mul_comm : ∀ (a b : QuotientCPolynomial R), a * b = b * a in CompPoly/Univariate/Quotient.lean moved from L684 to L704
def monomial [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L152 to L175
theorem evalEval_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L364 to L370
lemma degree_zero [Zero R] : degree (0 : CPolynomial R) = ⊥ in CompPoly/Univariate/Basic.lean moved from L562 to L634
theorem evalX_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L530 to L533
def pow [Semiring R] [BEq R] (p : CPolynomial.Raw R) (n : Nat) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L94 to L92
lemma coeff_extract_succ [Zero R] (a : CPolynomial.Raw R) (i : ℕ) : in CompPoly/Univariate/Basic.lean moved from L382 to L434
lemma sub_eq_add_neg : ∀ (a b : QuotientCPolynomial R), a - b = a + -b in CompPoly/Univariate/Quotient.lean moved from L516 to L545
theorem trim_twice [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Core.lean moved from L338 to L349
theorem canonical_ext [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L438 to L477
theorem support_toPoly_outer {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L398 to L401
def mulPowX {R : Type*} [Zero R] (i : ℕ) (p : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L364 to L370
theorem coeff_mul_X_zero [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L377 to L429
theorem leadingCoeffX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L778 to L779
lemma mul_equiv₂ [Semiring R] [BEq R] [LawfulBEq R] (a b₁ b₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L219 to L220
theorem Raw.eval₂_toPoly {R : Type*} [Semiring R] {S : Type*} [Semiring S] in CompPoly/Univariate/ToPoly/Equiv.lean moved from L189 to L187
def supportY {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : Finset ℕ in CompPoly/Bivariate/Basic.lean moved from L126 to L141
lemma mul_assoc [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L622 to L691
lemma toImpl_add {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] (p q : R[X]) : in CompPoly/Bivariate/ToPoly.lean moved from L128 to L130
theorem swap_toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L671 to L672
def leadingCoeffX {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] in CompPoly/Bivariate/Basic.lean moved from L179 to L198
def degree [Zero R] (p : CPolynomial R) : WithBot ℕ in CompPoly/Univariate/Basic.lean moved from L156 to L180
lemma zero_mul [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 * p = 0 in CompPoly/Univariate/Basic.lean moved from L626 to L696
theorem evalX_toPoly_eval_commute {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L555 to L558
def mulPowX [Zero R] (i : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L79 to L76
def trim [Zero R] [BEq R] (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Core.lean moved from L74 to L71
lemma mul_trim_equiv [Semiring R] [BEq R] [LawfulBEq R] (a b : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L192 to L193
def mulPowXDescending [Zero R] (i : ℕ) (p : CPolynomial.Raw R) : QuotientCPolynomial R in CompPoly/Univariate/Quotient.lean moved from L351 to L357
instance [Semiring R] [BEq R] [LawfulBEq R] : Module R (CPolynomial R) where in CompPoly/Univariate/Basic.lean moved from L47 to L1040
lemma eval₂_C {R : Type*} [Semiring R] {S : Type*} [Semiring S] in CompPoly/Univariate/ToPoly/Equiv.lean moved from L77 to L76
theorem natDegree_eq_support_sup [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : in CompPoly/Univariate/Basic.lean moved from L572 to L638
def mul [Semiring R] [BEq R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L89 to L87
lemma pow_is_trimmed [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L642 to L714
lemma coeff_zero [Zero R] (i : ℕ) : coeff (0 : CPolynomial R) i = 0 in CompPoly/Univariate/Basic.lean moved from L210 to L246
theorem size_eq_natDegree_of_zero [Zero R] [BEq R] in CompPoly/Univariate/Raw/Core.lean moved from L224 to L230
lemma mul_zero [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p * 0 = 0 in CompPoly/Univariate/Basic.lean moved from L630 to L700
theorem ofPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L182 to L185
lemma X_mul_divX_add [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L403 to L456
def eval₂ {S : Type*} [Semiring R] [Semiring S] in CompPoly/Univariate/Basic.lean moved from L174 to L205
theorem add_assoc [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L80 to L95
theorem eval_eq_sum_support [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (x : R) : in CompPoly/Univariate/Basic.lean moved from L275 to L317
lemma add_mul [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L638 to L709
def X {n : ℕ} {R : Type} [Zero R] [One R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L53 to L53
theorem coeff_eq_getElem_of_lt [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L242 to L249
theorem non_zero_map [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L418 to L456
def add [Zero R] [Add R] [BEq R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L53 to L50
lemma lastNonzero_unique [Zero Q] {p : CPolynomial.Raw Q} {k k' : Fin p.size} : in CompPoly/Univariate/Raw/Core.lean moved from L138 to L142
def swap {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] in CompPoly/Bivariate/Basic.lean moved from L167 to L185
instance Raw.instSetoidCPolynomial [Zero R] : Setoid (CPolynomial.Raw R) where in CompPoly/Univariate/Quotient.lean moved from L53 to L53
lemma zero_smul [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (0 : R) • p = 0 in CompPoly/Univariate/Basic.lean moved from L966 to L1021
lemma add_zero_equiv {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L105 to L106
def natDegreeX {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : ℕ in CompPoly/Bivariate/Basic.lean moved from L140 to L155
lemma smul_zero [Semiring R] [BEq R] [LawfulBEq R] (r : R) : r • (0 : CPolynomial R) = 0 in CompPoly/Univariate/Basic.lean moved from L937 to L990
lemma zipIdx_trim_append {R : Type*} [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L161 to L162
def negDescending [Zero R] [Neg R] (p : CPolynomial.Raw R) : QuotientCPolynomial R in CompPoly/Univariate/Quotient.lean moved from L308 to L312
lemma sub_descends [Ring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L329 to L335
theorem X_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] : in CompPoly/Bivariate/ToPoly.lean moved from L474 to L477
def Y {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] : in CompPoly/Bivariate/Basic.lean moved from L114 to L126
lemma coeff_C_mul [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L315 to L363
lemma pow_succ_right [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L653 to L725
def sub [Zero R] [Add R] [Neg R] [BEq R] in CompPoly/Univariate/Raw/Ops.lean moved from L133 to L130
theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT (R in CompPoly/Univariate/ToPoly/Degree.lean moved from L192 to L186
def X {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CBivariate R in CompPoly/Bivariate/Basic.lean moved from L111 to L122
lemma smul_descends [Semiring R] (r : R) (p₁ p₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L270 to L272
theorem degreeLT_mono {m n : ℕ} (h : m ≤ n) : in CompPoly/Univariate/ToPoly/Degree.lean moved from L197 to L190
lemma zero_add_equiv (p : CPolynomial.Raw R) : 0 + p ≈ p in CompPoly/Univariate/Quotient.lean moved from L449 to L463
theorem nsmul_succ [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L100 to L118
theorem toPoly_eq_map {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L215 to L219
theorem evalY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L632 to L635
def divX [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L193 to L226
def mulStep {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L124 to L125
theorem lastNonzero_none [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} : in CompPoly/Univariate/Raw/Core.lean moved from L107 to L110
def nsmulRaw [Semiring R] (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L65 to L62
def nsmul {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) in CompPoly/Univariate/Quotient.lean moved from L303 to L306
def nsmul [Semiring R] [BEq R] (n : ℕ) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L70 to L67
lemma coeff_X_mul_zero [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L344 to L394
theorem coeff_toPoly_Y {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L425 to L428
lemma leadingCoeff_eq_coeff_natDegree [Zero R] (p : CPolynomial R) : in CompPoly/Univariate/Basic.lean moved from L784 to L863
lemma mul_smul [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L978 to L1033
def natDegreeY {R : Type*} [Zero R] (f : CBivariate R) : ℕ in CompPoly/Bivariate/Basic.lean moved from L135 to L150
def monic [Zero R] [One R] [BEq R] (p : CPolynomial R) : Bool in CompPoly/Univariate/Basic.lean moved from L190 to L223
theorem CC_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (r : R) : in CompPoly/Bivariate/ToPoly.lean moved from L463 to L466
def eval [Semiring R] (x : R) (p : CPolynomial R) : R in CompPoly/Univariate/Basic.lean moved from L170 to L200
def pow {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L417 to L425
lemma pow_succ_left (n : ℕ) (x : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L617 to L639
def powDescending [Semiring R] [BEq R] (p : CPolynomial.Raw R) (n : ℕ) : in CompPoly/Univariate/Quotient.lean moved from L393 to L400
lemma erase_canonical [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L764 to L840
theorem degreeLT_succ_eq_degreeLE {n : ℕ} : in CompPoly/Univariate/ToPoly/Degree.lean moved from L200 to L195
def CC {R : Type*} [Zero R] [BEq R] [LawfulBEq R] (r : R) : CBivariate R in CompPoly/Bivariate/Basic.lean moved from L108 to L118
theorem induct [Zero R] [BEq R] [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} in CompPoly/Univariate/Raw/Core.lean moved from L184 to L188
def totalDegree {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : ℕ in CompPoly/Bivariate/Basic.lean moved from L145 to L160
def leadingCoeff [Zero R] [BEq R] (p : CPolynomial.Raw R) : R in CompPoly/Univariate/Raw/Core.lean moved from L97 to L94
theorem lastNonzero_some [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L116 to L119
lemma nsmul_succ : ∀ (n : ℕ) (x : QuotientCPolynomial R), in CompPoly/Univariate/Quotient.lean moved from L506 to L511
instance [Semiring R] [BEq R] [LawfulBEq R] : Pow (QuotientCPolynomial R) Nat in CompPoly/Univariate/Quotient.lean moved from L659 to L441
theorem nsmul_zero [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : nsmul 0 p = 0 in CompPoly/Univariate/Basic.lean moved from L97 to L114
theorem canonical_of_size_zero [Zero R] [BEq R] {p : CPolynomial.Raw R} : in CompPoly/Univariate/Raw/Core.lean moved from L349 to L361
theorem canonical_nonempty_iff [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L354 to L367
theorem natDegreeY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L408 to L411
lemma mulStep_zero {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L136 to L137
theorem toPoly_ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L255 to L260
def mul {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L388 to L395
theorem ofPoly_toPoly [BEq R] [LawfulBEq R] (q : QuotientCPolynomial R) : in CompPoly/Univariate/QuotientEquiv.lean moved from L65 to L63
theorem degree_eq_natDegree [Zero R] (p : CPolynomial R) (hp : p ≠ 0) : in CompPoly/Univariate/Basic.lean moved from L553 to L620
lemma coeff_monomial [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L225 to L261
def rename {n m : ℕ} {R : Type} [Zero R] [Add R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L207 to L207
def lcoeff (n : ℕ) : (CPolynomial R) →ₗ[R] R where in CompPoly/Univariate/Linear.lean moved from L25 to L25
lemma eq_degree_of_equiv [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial.Raw R} : in CompPoly/Univariate/Raw/Core.lean moved from L282 to L291
lemma zsmul_zero' : ∀ (a : QuotientCPolynomial R), zsmulRec nsmulRec 0 a = 0 in CompPoly/Univariate/Quotient.lean moved from L703 to L725
def natDegree [Zero R] (p : CPolynomial R) : ℕ in CompPoly/Univariate/Basic.lean moved from L163 to L190
lemma add_assoc : ∀ (a b c : QuotientCPolynomial R), a + b + c = a + (b + c) in CompPoly/Univariate/Quotient.lean moved from L440 to L454
lemma nsmul_zero : ∀ (x : QuotientCPolynomial R), in CompPoly/Univariate/Quotient.lean moved from L496 to L501
theorem lastNonzero_last_iff [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L379 to L393
instance smul [Semiring R] [BEq R] [LawfulBEq R] : SMul R (CPolynomial R) where in CompPoly/Univariate/Basic.lean moved from L927 to L979
lemma coeff_smul [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L931 to L983
def smul {R : Type*} [Semiring R] (r : R) (p : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L281 to L283
lemma coeff_erase [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L775 to L853
theorem coeff_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L387 to L393
lemma add_equiv {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L81 to L82
lemma degree_eq_support_max_aux_degree [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L500 to L556
lemma foldl_mulStep_zeros {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L145 to L146
def monomialXY {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] in CompPoly/Bivariate/Basic.lean moved from L117 to L131
theorem coeff_eq_coeff [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Raw/Core.lean moved from L260 to L268
theorem trim_equiv [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Core.lean moved from L335 to L345
lemma toPoly_prod.{u} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/ToPoly/Equiv.lean moved from L139 to L138
lemma zero_add : ∀ (a : QuotientCPolynomial R), 0 + a = a in CompPoly/Univariate/Quotient.lean moved from L458 to L472
lemma coeff_sub [Ring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L843 to L896
def canonical [Zero R] [BEq R] (p : CPolynomial.Raw R) : Prop in CompPoly/Univariate/Raw/Core.lean moved from L100 to L103
def sub [Add R] [Neg R] (p₁ p₂ : Lawful n R) : Lawful n R in CompPoly/Multivariate/Lawful.lean moved from L203 to L203
lemma mulPowX_descends [Zero R] (i : ℕ) (p₁ p₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L354 to L360
def coeff {R : Type*} [Zero R] (f : CBivariate R) (i j : ℕ) : R in CompPoly/Bivariate/Basic.lean moved from L122 to L137
lemma coeff_X_mul_succ [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L325 to L374
def erase [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L770 to L847
def neg {R : Type*} [NegZeroClass R] (p : QuotientCPolynomial R) : QuotientCPolynomial R in CompPoly/Univariate/Quotient.lean moved from L322 to L327
def equiv [Zero R] (p q : CPolynomial.Raw R) : Prop in CompPoly/Univariate/Raw/Core.lean moved from L273 to L282
lemma toPoly_zero {R : Type*} [Semiring R] : (0 : CPolynomial R).toPoly = 0 in CompPoly/Univariate/ToPoly/Equiv.lean moved from L105 to L103
def natDegreeBound [Zero R] (p : CPolynomial R) : Nat in CompPoly/Univariate/Basic.lean moved from L187 to L220
def mod [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L911 to L965
def coeff [Zero R] (p : CPolynomial R) (i : ℕ) : R in CompPoly/Univariate/Basic.lean moved from L137 to L158
lemma coeff_one [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i : ℕ) : in CompPoly/Univariate/Basic.lean moved from L214 to L251
def coeff [Zero R] (p : CPolynomial.Raw R) (i : ℕ) : R in CompPoly/Univariate/Raw/Core.lean moved from L50 to L47
def leadingCoeffY {R : Type*} [Zero R] (f : CBivariate R) : CPolynomial R in CompPoly/Bivariate/Basic.lean moved from L174 to L193
theorem ofPoly_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L245 to L249
lemma mulPowX_equiv {R : Type*} [Zero R] in CompPoly/Univariate/Quotient.lean moved from L93 to L94
def supportX {R : Type*} [Zero R] [BEq R] (f : CBivariate R) : Finset ℕ in CompPoly/Bivariate/Basic.lean moved from L130 to L145
lemma one_mul [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L610 to L677
lemma divX_size_lt [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (hp : p.val.size > 0) : in CompPoly/Univariate/Basic.lean moved from L453 to L509
theorem size_eq_natDegree_plus_one [Zero R] [BEq R] in CompPoly/Univariate/Raw/Core.lean moved from L217 to L222
theorem evalX_toPoly_eval {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [CommSemiring R] in CompPoly/Bivariate/ToPoly.lean moved from L595 to L598
def CPolynomial (R : Type*) [Zero R] in CompPoly/Univariate/Basic.lean moved from L35 to L36
theorem lastNonzero_spec [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} {k} : in CompPoly/Univariate/Raw/Core.lean moved from L121 to L125
lemma push_trim [Zero R] [BEq R] [LawfulBEq R] (arr : Array R) (c : R) : in CompPoly/Univariate/Raw/Core.lean moved from L411 to L449
def totalDegree {R : Type} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ in CompPoly/Multivariate/CMvPolynomial.lean moved from L141 to L142
instance [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommSemiring (CPolynomial R) where in CompPoly/Univariate/Basic.lean moved from L748 to L826
lemma toPoly_neg {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : in CompPoly/Univariate/ToPoly/Equiv.lean moved from L28 to L27
def size [Zero R] (p : CPolynomial R) : ℕ in CompPoly/Univariate/Basic.lean moved from L181 to L214
lemma mul_one [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L616 to L684
def degreeLE (n : WithBot ℕ) : Set (CPolynomial R) in CompPoly/Univariate/Linear.lean moved from L31 to L37
def sumToIter {n : ℕ} {R : Type} [Zero R] [Add R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L216 to L216
theorem lastNonzero_some_iff [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial.Raw R} {k} : in CompPoly/Univariate/Raw/Core.lean moved from L149 to L153
theorem canonical_empty [Zero R] [BEq R] : (mk (R in CompPoly/Univariate/Raw/Core.lean moved from L342 to L354
def CBivariate (R : Type*) [Zero R] in CompPoly/Bivariate/Basic.lean moved from L30 to L30
def divByMonic [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L899 to L953
theorem toPoly_coeff {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L205 to L209
theorem leadingCoeffY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L654 to L657
theorem monomial_add [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L242 to L280
theorem degree_eq_support_max [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L543 to L610
lemma ofPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : in CompPoly/Bivariate/ToPoly.lean moved from L303 to L309
lemma mulPowX_zero_equiv {R : Type*} [Zero R] in CompPoly/Univariate/Quotient.lean moved from L116 to L117
theorem eval₂_toPoly {R : Type*} [Semiring R] {S : Type*} [Semiring S] in CompPoly/Univariate/ToPoly/Equiv.lean moved from L200 to L199
def support [Zero R] [BEq R] (p : CPolynomial R) : Finset ℕ in CompPoly/Univariate/Basic.lean moved from L177 to L210
lemma mul_add [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L634 to L704
theorem size_le_size [Zero R] [BEq R] (p : CPolynomial.Raw R) : p.trim.size ≤ p.size in CompPoly/Univariate/Raw/Core.lean moved from L234 to L241
def erase [Zero R] [Add R] [Neg R] [BEq R] [DecidableEq R] in CompPoly/Univariate/Raw/Ops.lean moved from L140 to L139
theorem Y_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] : in CompPoly/Bivariate/ToPoly.lean moved from L484 to L487
def map {R S : Type*} [Semiring R] [Semiring S] in CompPoly/Multilinear/Basic.lean moved from L310 to L307
theorem natDegreeX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L437 to L440
lemma coeff_add [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L221 to L256
def X [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L143 to L165
lemma degree_eq_support_max_aux_lastNonzero [Zero R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L507 to L572
lemma monomial_add_erase [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/Basic.lean moved from L814 to L879
def neg [Neg R] (p : Lawful n R) : Lawful n R in CompPoly/Multivariate/Lawful.lean moved from L197 to L197
lemma mulStep_equiv {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L129 to L130
lemma nsmul_descends [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) in CompPoly/Univariate/Quotient.lean moved from L289 to L291
def evalY {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Bivariate/Basic.lean moved from L155 to L171
def nsmul [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L94 to L109
def C [Zero R] [BEq R] [LawfulBEq R] (r : R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L140 to L161
def lastNonzero [Zero R] [BEq R] (p : CPolynomial.Raw R) : Option (Fin p.size) in CompPoly/Univariate/Raw/Core.lean moved from L69 to L66
lemma neg_add_cancel : ∀ (a : QuotientCPolynomial R), -a + a = 0 in CompPoly/Univariate/Quotient.lean moved from L487 to L536
theorem eq_zero_iff_coeff_zero [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} : in CompPoly/Univariate/Basic.lean moved from L250 to L289
lemma toPoly_sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : in CompPoly/Univariate/ToPoly/Equiv.lean moved from L41 to L40
theorem eq_iff_coeff [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial R} : in CompPoly/Univariate/Basic.lean moved from L235 to L273
lemma Raw.toPoly_zero {R : Type*} [Semiring R] : (0 : CPolynomial.Raw R).toPoly = 0 in CompPoly/Univariate/ToPoly/Equiv.lean moved from L102 to L100
lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] : in CompPoly/Bivariate/ToPoly.lean moved from L295 to L301
def subDescending [Ring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Quotient.lean moved from L326 to L331
lemma commute_pow_self (n : ℕ) (x : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L632 to L653
def mulX [Zero R] (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L83 to L81
theorem divX_mul_X_add [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L433 to L487
def mulX [Zero R] (p : QuotientCPolynomial R) : QuotientCPolynomial R in CompPoly/Univariate/Quotient.lean moved from L370 to L376
lemma smul_eq_of_coeff_eq [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial R} in CompPoly/Univariate/Basic.lean moved from L943 to L996
def div [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L907 to L961
lemma pow_descends [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p₁ p₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L396 to L404
lemma coeff_divX [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : in CompPoly/Univariate/Basic.lean moved from L391 to L443
theorem degreeLTEquiv_toPoly [DecidableEq R] {n : ℕ} {p : CPolynomial R} in CompPoly/Univariate/ToPoly/Degree.lean moved from L133 to L275
lemma one_smul [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (1 : R) • p = p in CompPoly/Univariate/Basic.lean moved from L973 to L1028
lemma mem_support_iff [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : in CompPoly/Univariate/Basic.lean moved from L254 to L294
theorem supportX_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L503 to L506
theorem totalDegree_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L516 to L519
theorem induction_on [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L466 to L522
theorem eval₂_eq_sum_support {S : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Semiring S] in CompPoly/Univariate/Basic.lean moved from L300 to L341
lemma add_zero : ∀ (a : QuotientCPolynomial R), a + 0 = a in CompPoly/Univariate/Quotient.lean moved from L466 to L480
lemma one_is_trimmed [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : in CompPoly/Univariate/Basic.lean moved from L116 to L136
lemma mul_assoc (a b c : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L541 to L564
lemma toPoly_sum.{u} {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] {ι : Type u} in CompPoly/Univariate/ToPoly/Equiv.lean moved from L130 to L128
lemma smul_zero_equiv {R : Type*} [Semiring R] (p : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L73 to L74
def polyCoe (p : Lawful n R) : Lawful (n + 1) R in CompPoly/Multivariate/Lawful.lean moved from L257 to L242
lemma neg_descends [NegZeroClass R] (a b : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L311 to L315
def modByMonic [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean moved from L903 to L957
lemma coeff_neg [Ring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L840 to L892
lemma Raw.toPoly_C {R : Type*} [Semiring R] (r : R) : in CompPoly/Univariate/ToPoly/Equiv.lean moved from L85 to L84
theorem add_comm [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p + q = q + p in CompPoly/Univariate/Basic.lean moved from L77 to L91
def smul [Mul R] (r : R) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L60 to L57
def evalX {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Bivariate/Basic.lean moved from L150 to L165
lemma add_smul [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L960 to L1014
theorem erase_toPoly {R : Type*} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] in CompPoly/Univariate/ToPoly/Degree.lean moved from L83 to L97
lemma mul_equiv [Semiring R] [BEq R] [LawfulBEq R] (a₁ a₂ b : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L210 to L211
def add {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] (p q : QuotientCPolynomial R) : in CompPoly/Univariate/Quotient.lean moved from L262 to L264
lemma mul_comm [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p * q = q * p in CompPoly/Univariate/Basic.lean moved from L737 to L815
lemma coeff_eq_zero [Zero Q] {p : CPolynomial.Raw Q} : in CompPoly/Univariate/Raw/Core.lean moved from L276 to L285
def natDegree [Zero R] [BEq R] (p : CPolynomial.Raw R) : ℕ in CompPoly/Univariate/Raw/Core.lean moved from L90 to L87
def X [Zero R] [One R] : CPolynomial.Raw R in CompPoly/Univariate/Raw/Core.lean moved from L56 to L53
theorem elim [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Core.lean moved from L201 to L205
lemma C_mul_X_pow_eq_monomial [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] [Nontrivial R] in CompPoly/Univariate/Basic.lean moved from L702 to L782
theorem lastNonzero_induct [Zero R] [BEq R] [LawfulBEq R] {motive : CPolynomial.Raw R → Prop} in CompPoly/Univariate/Raw/Core.lean moved from L165 to L169
lemma ofPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L155 to L157
lemma add_descends [Semiring R] [BEq R] [LawfulBEq R] (a₁ b₁ a₂ b₂ : CPolynomial.Raw R) : in CompPoly/Univariate/Quotient.lean moved from L247 to L249
def neg [Neg R] (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L129 to L126
theorem toPoly_mul {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L231 to L235
theorem monomialXY_toPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L492 to L495
lemma smul_add [Semiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean moved from L949 to L1002
def lastNonzeroProp [Zero R] {p : CPolynomial.Raw R} (k : Fin p.size) : Prop in CompPoly/Univariate/Raw/Core.lean moved from L134 to L138
lemma toPoly_add {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L59 to L59
def addRaw [Zero R] [Add R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean moved from L47 to L44
lemma ofPoly_monomial {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean moved from L116 to L117
theorem zero_add [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 + p = p in CompPoly/Univariate/Basic.lean moved from L85 to L100
def leadingCoeff [Zero R] (p : CPolynomial R) : R in CompPoly/Univariate/Basic.lean moved from L167 to L197
theorem eq_of_equiv [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial.Raw R} : in CompPoly/Univariate/Raw/Core.lean moved from L313 to L322
lemma eq_to_equiv [Zero R] (p q : CPolynomial.Raw R) : p = q → p ≈ q in CompPoly/Univariate/Quotient.lean moved from L70 to L69
def smulDescending [Semiring R] (r : R) (p : CPolynomial.Raw R) : QuotientCPolynomial R in CompPoly/Univariate/Quotient.lean moved from L267 to L269

sorry Tracking

No sorrys were added, removed, or affected.

🎨 **Style Guide Adherence**

There are more than 20 violations of the style guide. They are grouped below by rule with representative examples:

Functions: Prefer fun x ↦ ... over λ x, ...
- Total Violations: 32
- The repository explicitly prefers the ↦ (maps to) syntax for function definitions over the standard => or legacy λ.
- Representative Examples:
  - CompPoly/Multilinear/Basic.lean:174: Vector.map (fun a => f a) p
  - CompPoly/Univariate/Basic.lean:192: (Finset.range p.val.size).filter (fun i => p.val.coeff i != 0)
  - CompPoly/Univariate/ToPoly/Equiv.lean:183: fun p => p.toPoly.eval x
Delimiters: Avoid parentheses where possible.
- Total Violations: 18
- The guide requires using pipes (<|, |>) or removing redundant parentheses, especially around simple function applications and simpa arguments.
- Representative Examples:
  - CompPoly/Univariate/Basic.lean:450: simpa using (coeff_divX (p := p) (i := n))
  - CompPoly/Univariate/Basic.lean:568: simpa using (Finset.le_sup (f := fun m => m) hn_mem)
  - CompPoly/Univariate/ToPoly/Equiv.lean:125: (toPoly_monomial (R := R) 1 (CPolynomial.C 1))
Documentation Standards: Use LaTeX for math: $ f(x) = y $ (inline)
- Total Violations: 6
- Mathematical expressions in docstrings or module headers must be enclosed in LaTeX delimiters.
- Representative Examples:
  - CompPoly/Univariate/Basic.lean:187: f(a₀) + f(a₁)*x + f(a₂)*x² + ...
  - CompPoly/Univariate/Basic.lean:223: coeff (divX p) i = coeff p (i + 1)
  - CompPoly/Univariate/Raw/Core.lean:57: c * X^n

📄 **Per-File Summaries**

AGENTS.md: This update introduces guidelines for typeclass minimization, instructing contributors to state the most restrictive requirements for each declaration instead of using broad section-level variables. It also adds a reference to a new documentation file, docs/wiki/typeclass-minimization.md, which provides detailed guidance on this practice.
CompPoly/Bivariate/Basic.lean: This change refactors the CBivariate definition and its associated operations to use more granular typeclass constraints, notably relaxing the requirement for the base type from a Semiring to just Zero where possible. It simplifies several algebraic instance declarations using inferInstanceAs and organizes the file into sections based on the required algebraic structures. No new theorems were added, and no sorry or admit placeholders were introduced.
CompPoly/Bivariate/ToPoly.lean: The changes in this file generalize the algebraic requirements for the base type R by replacing Ring and CommRing constraints with Semiring and CommSemiring across all definitions and theorems. The PR also updates internal calls to use isCanonical_toImpl instead of trim_toImpl and refactors several proofs, such as coeff_toPoly and leadingCoeffY_toPoly, to be more concise. No sorry or admit placeholders were introduced.
CompPoly/Multilinear/Basic.lean: This change generalizes multilinear polynomial operations by relaxing algebraic requirements from commutative rings to (commutative) semirings. Specifically, it updates the map and evaluation functions for both CMlPolynomial and CMlPolynomialEval to support these broader typeclass constraints.
CompPoly/Multilinear/Equiv.lean: This change generalizes the type class constraint on the ring R from CommRing to CommSemiring. This broadens the applicability of the file's multilinear equivalence results to a wider range of algebraic structures without modifying existing proofs or introducing new theorems.
CompPoly/Multivariate/CMvPolynomial.lean: This update generalizes the definitions of the variable $X_i$ and totalDegree by relaxing their typeclass requirements from CommSemiring to more basic constraints like Zero and One. These changes modify existing definitions to increase their applicability without introducing any new theorems or sorry placeholders.
CompPoly/Multivariate/Lawful.lean: This update generalizes polynomial operations by relaxing typeclass constraints from CommRing to specific algebraic requirements (such as Neg, Add, and Mul) and assigns low priority to heterogeneous operator instances to prevent conflicts with same-arity operations. The changes modify existing definitions and instances for negation, subtraction, and multiplication without introducing any sorry or admit placeholders.
CompPoly/Multivariate/MvPolyEquiv/Instances.lean: This change refactors the proof of the map_sub lemma for CMvPolynomial by using the change tactic to more directly target the underlying subtraction definition. It modifies an existing proof and contains no sorry or admit placeholders.
CompPoly/Multivariate/Operations.lean: This change generalizes the rename and sumToIter definitions by weakening the required typeclass constraints on the scalar type R from CommSemiring to Zero and Add. No new theorems or sorry placeholders were introduced.
CompPoly/Univariate/Basic.lean: The changes redefine CPolynomial R to track canonicity semantically through an IsCanonical predicate, allowing many definitions and theorems (like coeff, degree, and size) to have their typeclass requirements relaxed from Semiring to Zero or BEq. The refactor updates numerous proofs and algebraic instances to align with this new representation and improves the inheritance structure for semiring and ring implementations. No sorry or admit placeholders were added.
CompPoly/Univariate/Linear.lean: This file redefines bounded-degree polynomial predicates (degreeLE, degreeLT) to use the internal degreeBound property rather than abstract submodule kernels. It introduces several theorems proving closure under linear operations and provides new AddCommMonoid and Module instances for the resulting subtypes.
CompPoly/Univariate/Quotient.lean: The changes generalize the algebraic properties of QuotientCPolynomial by relaxing typeclass requirements from Ring to weaker structures like Semiring, Zero, or AddCommMonoid where appropriate. This refactoring updates existing definitions and proofs to support a broader range of base types and introduces a new AddCommMonoid instance. No sorry or admit placeholders were introduced.
CompPoly/Univariate/QuotientEquiv.lean: This update generalizes the algebraic requirements from Ring to Semiring and refactors type class constraints to only require BEq and LawfulBEq where strictly necessary, such as for the ringEquiv definition and the ofPoly_toPoly theorem. No sorry or admit placeholders were introduced.
CompPoly/Univariate/Raw/Core.lean: The changes refactor the file to use more granular typeclass constraints (such as Zero, One, and BEq instead of Semiring) and introduce the IsCanonical definition to represent polynomials with no trailing zeros. This update adds several new theorems relating canonicality to the trim operation and provides a stronger extensionality result (isCanonical_ext) for canonical polynomials. No sorry or admit placeholders were introduced.
CompPoly/Univariate/Raw/Division.lean: This change generalizes the Division section by removing the unnecessary Ring R typeclass constraint from the section variables. No new definitions or theorems are introduced, and no sorry placeholders are added.
CompPoly/Univariate/Raw/Ops.lean: This change refines the typeclass requirements for polynomial operations and instances in CPolynomial.Raw by replacing broad, section-wide Semiring variables with more granular constraints (e.g., [Zero R], [Add R], or [Neg R]). These modifications make the definitions and instances more generic, allowing them to be used with a wider range of algebraic structures. No new theorems were introduced, and no sorry or admit placeholders were added.
CompPoly/Univariate/Raw/Proofs.lean: This change generalizes the neg_coeff lemma by moving it outside the Ring section and weakening its typeclass requirements to NegZeroClass. The proof is slightly refactored for conciseness, and no sorry placeholders are introduced.
CompPoly/Univariate/ToPoly/Core.lean: This update generalizes the typeclass requirements for polynomial conversions from Ring to Semiring and introduces the isCanonical_toImpl theorem. Several proofs are refactored to leverage this new theorem, ensuring that conversions from mathlib polynomials to the internal raw representation maintain canonical form.
CompPoly/Univariate/ToPoly/Degree.lean: This file generalizes several results from Ring to Semiring and refactors proofs for degree-related theorems (such as degree_toPoly and leadingCoeff_toPoly) to be more direct and robust. It introduces new helper lemmas regarding implementation size and formally defines degreeLTEquiv as a LinearEquiv between polynomials of bounded degree and their coefficient vectors. No sorry or admit placeholders were added.
CompPoly/Univariate/ToPoly/Equiv.lean: This change generalizes several theorems and definitions by weakening type class requirements from Ring or Field to Semiring (or CommSemiring) where possible. It also updates the ringEquiv definition to use isCanonical_toImpl and simplifies several proofs, such as X_toPoly. No sorry or admit placeholders were introduced.
docs/wiki/README.md: This update adds a new entry to the documentation index for typeclass-minimization.md. This guide outlines best practices for maintaining minimal typeclass assumptions and managing instance scopes within the library.
docs/wiki/typeclass-minimization.md: This documentation introduces the "Typeclass Minimization" policy, which mandates using the weakest possible mathematical assumptions for all new Lean declarations. It provides practical guidelines, preferred coding styles, and specific examples of replacing broad structures like Ring with more targeted classes like Zero or NegZeroClass to avoid over-constraining definitions and theorems.
tests/CompPolyTests.lean: This change expands the test suite by importing additional modules for linear univariate polynomials and basic bivariate polynomials. No new theorems, definitions, or sorry placeholders are introduced in this file.
tests/CompPolyTests/Bivariate/Basic.lean: This file introduces basic regression tests for the CBivariate API and its transport to standard polynomials via toPoly. It includes proofs verifying properties of degrees, leading coefficients, and monomial evaluations, and contains no sorry or admit placeholders.
tests/CompPolyTests/Univariate/Linear.lean: This new test file introduces private definitions and theorems to verify the instance-stability of the CPolynomial API, ensuring that polynomials and bounded-degree subtypes can be reused across different lawful BEq instances without explicit casts. It provides regression tests for polynomial construction, arithmetic, and coefficient access in the univariate case; no sorry or admit placeholders are used.

Last updated: 2026-03-12 12:13 UTC.

github-actions · 2026-03-12T02:20:09Z

🤖 Initial AI review without external context

🤖 AI Review

Overall Summary:

Executive Summary

TL;DR:
This PR executes an excellent systematic refactor, successfully relaxing overly restrictive global typeclass constraints (such as [Semiring R] and [BEq R]) down to their mathematical minimums across the polynomial types. The underlying mathematical redesign is highly robust, though there is a conflicting typeclass instance regarding exponentiation that requires adjustment before merging.

Checklist Coverage:
No explicit specification checklist was provided for this review.

Key Lean 4 / Mathlib Issues:

Redundant and Conflicting HPow Instance (1 file):
In CompPoly/Multivariate/Lawful.lean, there is an explicit instance for HPow (Lawful n R) ℕ (Lawful n R) defined in the "Mixed-arity fallbacks" section. This must be removed for three reasons:
1. Redundancy: An instance [NatCast R] [Add R] [Mul R] : NatPow (Lawful n R) is correctly defined earlier in the file. Lean 4 automatically derives Pow α ℕ and HPow α ℕ α from NatPow.
2. Defeq Conflict: The explicit HPow instance evaluates via exp.iterate p₁.mul 1, whereas the derived NatPow instance uses npow (which evaluates recursively). Because these are not definitionally equal, maintaining both creates subtle rfl failures and typeclass ambiguities.
3. Categorization: Exponentiation by a natural number does not change the polynomial arity n, so it fundamentally does not belong in a "mixed-arity" fallback section.

Minor Polish & Nitpicks:

Redundant Typeclass Assumptions:
- In CompPoly/Bivariate/ToPoly.lean, toPoly_zero assumes [Nontrivial R]. Since toPoly dropped this requirement and 0 only depends on Zero, this assumption can be safely removed.
- In CompPoly/Univariate/ToPoly/Core.lean, the [Zero R] assumption on toPoly is redundant because [Semiring R] already implies it.
Variable Shadowing: In CompPoly/Univariate/Raw/Proofs.lean, explicitly declaring {R : Type*} in the signature of neg_coeff shadows the module-level variable declaration and will trigger the linter.shadowing warning. Rely on the implicit R instead.
Redundant Instance Fields: In CompPoly/Univariate/Quotient.lean, the Ring instance manually provides sub_eq_add_neg, zsmul, and related fields. Because these are already provided by (or default-inferred for) the AddCommGroup instance, they override the defaults unnecessarily and should be removed.
Tactic Robustness: In CompPoly/Multivariate/Lawful.lean, the definition of polyCoe uses cast (by simp). To prevent breakage from future simp set evolutions, prefer a precise structural tactic like by omega.
Eta Reduction: In CompPoly/Multilinear/Basic.lean, Vector.map (fun a => f a) p can be cleanly reduced to Vector.map f p in CMlPolynomialEval.map, leaning on the FunLike coercion.
Formatting: CompPoly/Univariate/ToPoly/Degree.lean contains a few 4-space indentations inside by blocks (standard is 2-space relative to the declaration/by keyword) and redundant parentheses around {p : (CPolynomial R)} in mem_degreeLE.

Overall Verdict: Changes Requested

📄 **Review for `CompPoly/Bivariate/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(Self-Correction/Sanity Check during review): The PR successfully relaxes overly restrictive global typeclass constraints (like [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R]) on the CBivariate type and cleanly localizes them to exactly the operations that require them. The reduction to [Zero R] for the type's definition is mathematically correct and aligns perfectly with CPolynomial, ensuring that unconstrained definitions (like coeff and natDegreeY) do not artificially require a semiring. All implementations properly handle the inner (X) / outer (Y) distinction. Excellent cleanup!

📄 **Review for `CompPoly/Bivariate/ToPoly.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Unnecessary typeclass assumption: In toPoly_zero, the [Nontrivial R] assumption appears to be a leftover from the previous signature of toPoly. Because toPoly dropped its Nontrivial R requirement and 0 : CBivariate R only depends on the Zero instance (which just relies on Zero R and does not need Nontrivial R), you can safely drop [Nontrivial R] from the lemma signature as well.
```
lemma toPoly_zero {R : Type*} [BEq R] [LawfulBEq R] [Semiring R] :
    toPoly (0 : CBivariate R) = 0 := by
```

📄 **Review for `CompPoly/Multilinear/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

In CMlPolynomialEval.map, you can simplify Vector.map (fun a => f a) p to Vector.map f p to match the updated implementation of CMlPolynomial.map, cleanly relying on the FunLike coercion for R →+* S.

📄 **Review for `CompPoly/Multilinear/Equiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/CMvPolynomial.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Lawful.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None. Relaxing the [CommRing R] constraint to fine-grained constraints like [Neg R] and [Add R] is mathematically sound and correctly expands the usability of these fundamental polynomial operations to weaker algebraic structures (e.g., generic semirings and additive groups).

Lean 4 / Mathlib Issues:

Redundant and Conflicting HPow Instance:
In the "Mixed-arity fallbacks" section, there is an explicit HPow instance:
```
instance (priority := low) [NatCast R] [Add R] [Mul R] :
    HPow (Lawful n R) ℕ (Lawful n R) :=
  ⟨fun p₁ exp ↦ exp.iterate p₁.mul 1⟩
```
This instance should be removed for several reasons:
1. Redundancy: Earlier in the file, you correctly define instance [NatCast R] [Add R] [Mul R] : NatPow (Lawful n R). In Lean 4, having a NatPow α instance automatically provides Pow α ℕ (via instPowNat) and HPow α ℕ α (via instHPow).
2. Defeq Conflict: The explicit HPow instance evaluates via exp.iterate p₁.mul 1, while the NatPow instance uses npow, which computes recursively as (npow n p) * p. Because these are not definitionally equal, having both can lead to subtle rfl failures and typeclass resolution ambiguities.
3. Categorization: Unlike HAdd and HMul, exponentiation takes a natural number on the right-hand side. There is no "mixed polynomial arity" occurring here (the polynomial arity n is the same before and after), so it doesn't fit the purpose of the fallback section.

Nitpicks:

Tactics in cast:
In the definition of polyCoe:
```
def polyCoe (p : Lawful n R) : Lawful (n + 1) R := cast (by simp) (p.extend n.succ)
```
Using by simp to prove max n (n + 1) = n + 1 works, but it can be slightly fragile in cast if the simp set evolves. It is generally more robust to use a precise structural tactic like by omega or a term proof using Nat.max_eq_right.
Fix: cast (by omega) (p.extend n.succ)

📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Instances.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The change to map_sub using change is a solid improvement over sequentially unfolding typeclass projections, making the proof more robust to underlying changes in instance names or definitions.)

📄 **Review for `CompPoly/Multivariate/Operations.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Univariate/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None.

Lean 4 / Mathlib Issues:
None.

Nitpicks:
None.

(The refactoring of CPolynomial to use a purely semantic IsCanonical predicate—which depends only on [Zero R] and not on the decidability of equality—is an excellent design choice. It successfully decouples the canonical representation from specific BEq instances, resolving potential instance coherence issues. Furthermore, tightening the typeclass assumptions across the file makes the API significantly more robust.)

📄 **Review for `CompPoly/Univariate/Linear.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Reviewer Notes:
The PR significantly improves the design of bounded-degree polynomials in the library. Replacing the unwieldy intersection of kernels (⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff S k)) with a clean Set (and providing the explicit subtype algebraic instances) is an excellent refactor. It prevents the leakage of non-computable submodule lattice infrastructure into what should be a straightforward, computable polynomial type, and it makes definitional equalities much friendlier to work with downstream. The proofs are clean, idiomatic, and leverage subtype coercions flawlessly. Excellent work.

📄 **Review for `CompPoly/Univariate/Quotient.lean`**

Verdict: Approved

Critical Misformalizations:
None. The weakening of typeclass assumptions (e.g., relaxing [Ring R] to [Zero R] or [Semiring R]) is mathematically correct and accurately tracks the minimal requirements for each operation.

Lean 4 / Mathlib Issues:
None. The use of Lean 4 quotient mechanics is idiomatic. Relying on auto-synthesis of parent structures (AddCommMonoid, AddCommGroup, Semiring) for the Ring instance without explicitly writing __ := inferInstance is perfectly valid and standard in newer Lean 4 versions.

Nitpicks:

Redundant fields in Ring instance: The PR elegantly breaks out the AddCommGroup instance so it's available for Ring R (and limits AddCommMonoid to Semiring R). However, the fields sub_eq_add_neg, zsmul, zsmul_zero', zsmul_succ', and zsmul_neg' are now provided by (or default-inferred for) the AddCommGroup instance. Providing them again inside the Ring instance is redundant and overrides the AddGroup defaults unnecessarily. You can clean up the Ring instance to simply be:
```
instance : Ring (QuotientCPolynomial R) where
  intCast_ofNat := by intro n; simp [IntCast.intCast]; rfl
  intCast_negSucc := by
    -- By definition of `Int.negSucc`, we have `Int.negSucc n = - (n + 1)`.
    have h_neg_succ : ∀ n : ℕ, Int.negSucc n = - (n + 1 : ℤ) := by grind
    convert h_neg_succ
    convert Quotient.eq using 1
    simp +decide [ Raw.instSetoidCPolynomial ]
    simp +decide [ Raw.C, Raw.neg ]
    grind
```
(The parent fields will be automatically populated from Semiring and AddCommGroup).

📄 **Review for `CompPoly/Univariate/QuotientEquiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Univariate/Raw/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Summary:
This is an excellent cleanup that systematically refines typeclass bounds. Removing the overly strong [Semiring R] and [BEq R] from the global section scope and shifting to minimal bounds ([Zero R], [One R], [LawfulBEq R]) for definitions like coeff, X, and trim makes the codebase much cleaner and mathematically precise.

The decoupling of the mathematical property IsCanonical (which only relies on propositional ≠ 0) from the computational p.trim = p (which relies on BEq and LawfulBEq) is a particularly great design choice, ensuring canonicality is an intrinsic property of the polynomial array rather than tied to a specific Boolean equality instance.

📄 **Review for `CompPoly/Univariate/Raw/Division.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Univariate/Raw/Ops.lean`**

Verdict: Approved

Critical Misformalizations:
None. The modifications preserve the semantic meaning of all operations while relaxing overly restrictive typeclass assumptions.

Lean 4 / Mathlib Issues:
None. This PR represents a substantial improvement in typeclass minimality. By removing the section-wide [Semiring R] [BEq R] and [Ring R] [BEq R] variables, the definitions and instances now require only their minimally necessary algebraic structures (e.g., [Add R] and [Zero R] for addRaw, [Mul R] for smul). This perfectly adheres to Mathlib's guidelines on keeping assumptions as weak as possible.

Nitpicks:
None.

📄 **Review for `CompPoly/Univariate/Raw/Proofs.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Shadowing module-level variables: The file declares variable {R : Type*} at the top level. In the newly moved neg_coeff lemma, {R : Type*} is explicitly declared in the signature, which shadows the module-level variable and can trigger Lean 4's linter.shadowing warning. You can just rely on the existing implicit R by dropping {R : Type*} from the binder list:
```
lemma neg_coeff [NegZeroClass R] (p : CPolynomial.Raw R) (i : ℕ) :
    p.neg.coeff i = - p.coeff i := by
```

📄 **Review for `CompPoly/Univariate/ToPoly/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Redundant Typeclass Assumption: In toPoly for CPolynomial R, the [Zero R] assumption is redundant because [Semiring R] already implies [Zero R]. Lean's typeclass synthesis will automatically resolve the [Zero R] required by CPolynomial R using the semiring instance.
```
noncomputable def toPoly [Semiring R] (p : CPolynomial R) : Polynomial R := p.val.toPoly
```

📄 **Review for `CompPoly/Univariate/ToPoly/Degree.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Indentation: The proofs for degree_le_iff_coeff_zero, degree_lt_iff_coeff_zero, and degreeLTEquiv_toPoly use a 4-space indent for the inner lines of the by block, whereas standard Lean 4 style usually calls for a 2-space indent relative to the theorem declaration (or the by keyword).
Unnecessary Parentheses: In theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} :, the parentheses around CPolynomial R are redundant and can be safely removed.

📄 **Review for `CompPoly/Univariate/ToPoly/Equiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Feedback:
This is an excellent set of cleanups and refactors! Weakening the global assumption from [Ring R] to [Semiring R] and isolating [Ring R] strictly to the lemmas that need it (toPoly_neg, toPoly_sub) greatly improves the generality of the file.

Furthermore, weakening [Field R] to [Semiring R] in toPoly_sum and [CommSemiring R] in toPoly_prod accurately captures the mathematical minimums. Adding [Nontrivial R] to ringEquiv is also mathematically correct since CPolynomial R requires it for its Semiring instance (since its 1 definition assumes $1 \neq 0$). Finally, fixing the invFun constructor in ringEquiv to use isCanonical_toImpl instead of trim_toImpl resolves a subtle type-checking property mismatch.

The strategy of shadowing the auto-inserted section variable {R : Type*} [Semiring R] by explicitly re-binding {R : Type*} [Semiring R] to drop the [BEq R] assumption (as done in eval₂_toPoly and others) is a perfectly fine and standard trick in Lean 4 to substitute the missing omit syntax. The replacement of expose_names with explicit change in X_toPoly is also a much cleaner proof structure.

Great work!

📄 **Review for `tests/CompPolyTests.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `tests/CompPolyTests/Bivariate/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `tests/CompPolyTests/Univariate/Linear.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Keep the instance-stability refactor decoupled from `BEq`, restore the missing bounded-degree subtype data instances, and expose the inherited `CBivariate` equality instances. Fold in the Lean style and test cleanups needed for the PR lint job to pass cleanly. Made-with: Cursor

quangvdao · 2026-03-12T08:21:04Z

Addressed the remaining Gemini follow-ups in a1c78e9.

decoupled degreeLE / degreeLT from the unnecessary [BEq] requirement
split Zero / Add / SMul data instances out from the richer degreeLT subtype algebraic instances
made Raw.IsCanonical and isCanonical_toImpl independent of the BEq hierarchy where intended
removed the redundant Ring additive fields and the unused DecidableEq assumption in leadingCoeff_eq_coeff_natDegree
exposed inherited BEq / LawfulBEq / DecidableEq instances on CBivariate
cleaned the Lean style issues that were failing the lint job, plus the test header and helper naming nits

Local validation:

python3 scripts/lint-style.py on the touched Lean files
lake build CompPolyTests

Push typeclass requirements down onto the raw and canonical polynomial APIs so computable declarations only require the structure they actually use. Update the univariate and bivariate bridge proofs to preserve the weaker signatures without regressing builds or tests. Made-with: Cursor

Tighten the most mechanical typeclass hypotheses on the raw univariate ops, bivariate core stubs, and multivariate core constructors so foundational APIs only require the structure they actually use. Keep the downstream bridge layer building by updating the one multivariate equivalence proof that unfolded the old autogenerated subtraction instance. Made-with: Cursor

Lower the univariate and bivariate toPoly bridges and the multilinear monomial-basis layer to semiring-level assumptions wherever the constructions only use additive and multiplicative structure. Keep the genuinely subtractive bridge facts explicitly ring-scoped so the API becomes tighter without changing behavior. Made-with: Cursor

Lower the remaining high-confidence bridge, quotient, and helper declarations to the weakest algebraic assumptions that match their implementations. Preserve existing inference behavior where mixed-arity multivariate fallbacks would otherwise compete with same-arity instances. Made-with: Cursor

Record the expectation that new Lean declarations should carry the weakest typeclass assumptions they actually need, avoid blanket section-level instance scopes, and point agents to concrete examples from the recent refactor. Made-with: Cursor

Remove the duplicated section variable in the multilinear monomial-basis helpers and generalize `CMlPolynomial.map` to the weaker semiring assumptions flagged in Gemini review. Made-with: Cursor

quangvdao · 2026-03-12T11:23:51Z

Addressed the remaining Gemini nits in cf00643.

removed the duplicated multilinear section variable
generalized CMlPolynomial.map to the weaker semiring assumptions the review called out

Local validation:

python3 scripts/lint-style.py CompPoly/Multilinear/Basic.lean
lake build CompPoly.Multilinear.Basic
lake test

dhsorens

this is kind of a huge PR that does a lot of things at once, and for that reason a bit hard to evaluate. In future, I would be grateful for more targeted PRs that are more feasible to evaluate. For large goals, incremental PRs should be the norm and we might even consider putting a standard expectation for max PR size. ~200–400 lines diff is ideal, once PRs exceed 500–800 lines, review quality drops significantly.

I see for e.g. that in CompPoly/Univariate/Linear.lean, bounded-degree objects were moved from being defined as a Submodule first to being defined as a Set predicate first, then the subtype ↥(degreeLT n) is given algebraic structure manually. The relevant definitions have been changed - what was the motivation for this? What does it give us? I assume that the definitions are still proved correct wrt Mathlib in ToPoly and so am not too fussed by them.

From what I can tell, this PR mainly does this from the PR summary

Transitions CPolynomial and CBivariate to a model tracking canonicity via an IsCanonical predicate (ensuring no trailing zeros). This enables core operations like coeff, degree, and size to function with minimal requirements such as Zero or BEq instead of full Semiring structures.

which I'm happy with especially since it removes the need for boolean equality across the board. I'm curious to know if IsCanonical will contribute to proof ergonomics in the upcoming projects and wary of implementing it if it is cumbersome to work with.

Lastly, NB we should probably consider merging (or no) #127 before a major refactor like this at the typeclass level.

dhsorens · 2026-03-12T16:16:31Z

Would it be possible to just make the IsCanonical change and then incrementally build from there? (Or is the PR the result of the IsCanonical change?) I would personally prefer to see the diff on that change alone to judge any tradeoffs. I suspect it is the better way to go but I don't want to go through a typeclass refactor only to discover something went wrong and not be able to really untangle it from this single PR

quangvdao · 2026-03-12T23:51:45Z

@dhsorens I split this refactor into a smaller replacement series from fresh branches off current master.

Replacement PRs

refactor(comp-poly): isolate canonical carrier transport #160 refactor(comp-poly): isolate canonical carrier transport
Base: master
refactor(comp-poly): rebuild bounded-degree API #161 refactor(comp-poly): rebuild bounded-degree API
Base: refactor(comp-poly): isolate canonical carrier transport #160
refactor(comp-poly): minimize raw and quotient assumptions #162 refactor(comp-poly): minimize raw and quotient assumptions
Base: refactor(comp-poly): isolate canonical carrier transport #160
refactor(comp-poly): weaken multivariate core assumptions #163 refactor(comp-poly): weaken multivariate core assumptions
Base: master
fix(comp-poly): clean up multilinear map assumptions #164 fix(comp-poly): clean up multilinear map assumptions
Base: master
refactor(comp-poly): minimize bivariate transport assumptions #165 refactor(comp-poly): minimize bivariate transport assumptions
Base: refactor(comp-poly): rebuild bounded-degree API #161

Notes

PR refactor(comp-poly): isolate canonical carrier transport #160 keeps the carrier cutover first and only carries the minimum bivariate bridge fallout needed to keep the repo building.
PR refactor(comp-poly): minimize bivariate transport assumptions #165 ended up stacking on the bounded-degree branch rather than the raw/quotient branch because the remaining CBivariate.toPoly minimization depends on the generalized degree-transport surface from PR refactor(comp-poly): rebuild bounded-degree API #161.

I’m closing this PR in favor of the smaller replacement stack above.

Merge branch 'master' into quang/cpoly-refactor

a3ad00f

quangvdao changed the title ~~refactor(comp-poly): make canonical carriers instance-stable~~ refactor(comp-poly): weaken the typeclass condition on CPolynomial and CBivariate Mar 12, 2026

quangvdao changed the title ~~refactor(comp-poly): weaken the typeclass condition on CPolynomial and CBivariate~~ refactor(comp-poly): canonicalize computable polynomials and weaken typeclasses Mar 12, 2026

quangvdao added 2 commits March 12, 2026 16:40

quangvdao requested a review from dhsorens March 12, 2026 10:11

quangvdao and others added 3 commits March 12, 2026 17:47

docs: add typeclass minimization guidance

92924f8

Record the expectation that new Lean declarations should carry the weakest typeclass assumptions they actually need, avoid blanket section-level instance scopes, and point agents to concrete examples from the recent refactor. Made-with: Cursor

Merge branch 'master' into quang/cpoly-refactor

f5cf966

quangvdao changed the title ~~refactor(comp-poly): canonicalize computable polynomials and weaken typeclasses~~ refactor(comp-poly): canonicalize polynomial APIs and tighten assumptions Mar 12, 2026

fix: clean up multilinear map assumptions

cf00643

Remove the duplicated section variable in the multilinear monomial-basis helpers and generalize `CMlPolynomial.map` to the weaker semiring assumptions flagged in Gemini review. Made-with: Cursor

Merge remote-tracking branch 'origin/master' into quang/cpoly-refactor

ed366b0

dhsorens reviewed Mar 12, 2026

View reviewed changes

quangvdao closed this Mar 12, 2026

quangvdao deleted the quang/cpoly-refactor branch March 17, 2026 05:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor(comp-poly): canonicalize polynomial APIs and tighten assumptions#154

refactor(comp-poly): canonicalize polynomial APIs and tighten assumptions#154
quangvdao wants to merge 11 commits intomasterfrom
quang/cpoly-refactor

quangvdao commented Mar 12, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 12, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 12, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 12, 2026 •

edited

Loading

Uh oh!

quangvdao commented Mar 12, 2026

Uh oh!

quangvdao commented Mar 12, 2026 •

edited

Loading

Uh oh!

dhsorens left a comment •

edited

Loading

Uh oh!

dhsorens commented Mar 12, 2026

Uh oh!

quangvdao commented Mar 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

quangvdao commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Key Changes

Testing

Review Guidance

Uh oh!

github-actions bot commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

github-actions bot commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Gemini PR Summary

Mathematical Refactoring and Generalization

Computability and Kernel Stability

Documentation and Infrastructure

Uh oh!

github-actions bot commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Initial AI review without external context

🤖 AI Review

Executive Summary

Uh oh!

quangvdao commented Mar 12, 2026

Uh oh!

quangvdao commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dhsorens left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dhsorens commented Mar 12, 2026

Uh oh!

quangvdao commented Mar 12, 2026

Replacement PRs

Notes

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

quangvdao commented Mar 12, 2026 •

edited

Loading

github-actions bot commented Mar 12, 2026 •

edited

Loading

github-actions bot commented Mar 12, 2026 •

edited

Loading

github-actions bot commented Mar 12, 2026 •

edited

Loading

quangvdao commented Mar 12, 2026 •

edited

Loading

dhsorens left a comment •

edited

Loading