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.