From 05cbdf2ab32e4b598da08f29aa59b8f1b9f871ec Mon Sep 17 00:00:00 2001
From: Derek Sorensen <d@dhsorens.com>
Date: Mon, 16 Feb 2026 13:23:51 +0000
Subject: [PATCH] feat: drop leadingMonomial in favor of leadingTerm

---
 CompPoly/Multivariate/CMvPolynomial.lean | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean
index dc0010e..8592b5b 100644
--- a/CompPoly/Multivariate/CMvPolynomial.lean
+++ b/CompPoly/Multivariate/CMvPolynomial.lean
@@ -162,14 +162,6 @@ class MonomialOrder (n : ℕ) where
 def MonomialOrder.degree {n : ℕ} [MonomialOrder n] (m : CMvMonomial n) : ℕ :=
   sorry
 
-/-- Leading monomial of a polynomial according to a monomial order.
-
-  Returns `none` for the zero polynomial.
--/
-def leadingMonomial {n : ℕ} {R : Type} [Zero R] [MonomialOrder n]
-    (p : CMvPolynomial n R) : Option (CMvMonomial n) :=
-  sorry
-
 /-- Leading coefficient of a polynomial according to a monomial order.
 
   Returns `0` for the zero polynomial.
@@ -178,6 +170,15 @@ def leadingCoeff {n : ℕ} {R : Type} [Zero R] [MonomialOrder n]
     (p : CMvPolynomial n R) : R :=
   sorry
 
+/-- Leading term of a polynomial according to a monomial order.
+
+  Equals `monomial (degree p) (leadingCoeff p)` when `p ≠ 0`, and `0` otherwise.
+  Matches Mathlib's `MonomialOrder.leadingTerm`.
+-/
+def leadingTerm {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n]
+    (p : CMvPolynomial n R) : CMvPolynomial n R :=
+  sorry
+
 /-- Multiset of all variable degrees appearing in the polynomial.
 
   Each variable `i` appears `degreeOf i p` times in the multiset.