issue 49 - leadingCoeff, leadingTerm, etc

[dhsorens]

Closes #49 ; WIP

[github-actions]

🤖 Gemini PR Summary

This Pull Request updates the multivariate polynomial API to better align with Mathlib conventions by replacing leadingMonomial with leadingTerm. This change streamlines the library's integration with the broader Lean ecosystem and addresses issue #49.

Features

• Standardized API: Introduced leadingTerm as the primary definition for the leading component of a multivariate polynomial, replacing the previous leadingMonomial naming convention.

Fixes

• Issue Implement monomial ordering functions: MonomialOrder.degree, leadingMonomial, leadingCoeff #49: Provides the core implementation for the transition to Mathlib-aligned polynomial terminology.

Refactoring

• Naming Alignment: Updated CompPoly/Multivariate/CMvPolynomial.lean to use leadingTerm, ensuring consistency with standard mathematical library structures in Lean.

---

Note: This PR is currently marked as Work In Progress (WIP).

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	9
❌ Lines Removed	8

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• def leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n] in CompPoly/Multivariate/CMvPolynomial.lean

❌ **Added:** 1 `sorry`(s)

• def leadingTerm {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] in CompPoly/Multivariate/CMvPolynomial.lean

---

🎨 **Style Guide Adherence**

Based on the provided style guide, here are the lines from the code changes that violate the guidelines:

Line 173: Equalsmonomial (degree p) (leadingCoeff p)whenp ≠ 0, and 0 otherwise.

• Violation: "Use LaTeX for math: $ f(x) = y $ (inline) or $$ \sum_{i=0}^n i $$ (display)." (The terms p ≠ 0 and 0 should be formatted as LaTeX).

Line 176: def leadingTerm {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n]

• Violation: "Use namespaces to group related definitions (e.g., List.map). This enables dot notation (e.g., l.map f) when the type is known." (Since the function operates on CMvPolynomial, it should be in that namespace to enable dot notation).
• Violation: "α, β, γ, ... : Generic types" (The variable R is used for a type where α or β is preferred).

Line 177: (p : CMvPolynomial n R) : CMvPolynomial n R :=

• Violation: "Use 2 spaces for indentation." (The line is indented 4 spaces).
• Violation: "p, q, r, ... : Predicates and relations" (The variable p is used for a polynomial element, but is reserved by the guide for predicates).

---

📄 **Per-File Summaries**

• CompPoly/Multivariate/CMvPolynomial.lean: Replaced the leadingMonomial definition with leadingTerm to better align the multivariate polynomial API with Mathlib conventions.

---

Last updated: 2026-02-16 13:26 UTC.