diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 4ee028d7c404a..53d3585e76d8f 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -332,8 +332,6 @@ def polyrith (g : MVarId) (only : Bool) (hyps : Array Expr)
     if hyps'.isEmpty then
       return ← byRing "polyrith did not find any relevant hypotheses"
     let vars := (← get).atoms.size
-    if vars = 0 then
-      return ← byRing "polyrith did not find find any variables"
     match ← sageOutput (createSageArgs traceOnly α vars hyps' tgt) with
     | .ok { trace, data } =>
       if let some trace := trace then logInfo trace
diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index f25beea928b36..0ced1a3ca1064 100644
--- a/scripts/polyrith_sage.py
+++ b/scripts/polyrith_sage.py
@@ -21,11 +21,15 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
     for a description of this method. """
     var_list = ", ".join([f"var{i}" for i in range(n_vars)])
     query = f'''
-P = PolynomialRing({type_str(type)}, 'var', {n_vars!r})
-[{var_list}] = P.gens()
-gens = {eq_list}
+if {n_vars!r} != 0:
+    P = PolynomialRing({type_str(type)}, 'var', {n_vars!r})
+    [{var_list}] = P.gens()
+else:
+    # workaround for a Sage shortcoming with `n_vars = 0`,
+    # `TypeError: no conversion of this ring to a Singular ring defined`
+    P = PolynomialRing({type_str(type)}, 'var', 1)
 p = P({goal_type})
-I = ideal(gens)
+I = P.ideal({eq_list})
 coeffs = p.lift(I)
 print(serialize_polynomials(coeffs))
 '''
diff --git a/test/polyrith.lean b/test/polyrith.lean
index 5123abc612765..b941ec56c1d4d 100644
--- a/test/polyrith.lean
+++ b/test/polyrith.lean
@@ -433,11 +433,27 @@ A full test suite is provided at the bottom of the file.
 --   "(1 - 2)"]
 --   "linear_combination h1 - h2"
 
+-- example {R} [CommRing R] (x : R) (h2 : (2 : R) = 0) : x + x = 0 :=
+-- by test_polyrith
+--   "{\"data\":[\"(poly.var 0)\"],\"success\":true}"
+--   ["ff",
+--   "R",
+--   "1",
+--   "[(2 - 0)]",
+--   "((var0 + var0) - 0)"]
+--   "linear_combination x * h2"
 
--- We comment the following tests so that we don't overwhelm the SageCell API.
-
-
+-- example {R} [CommRing R] (_x : R) (h : (2 : R) = 4) : (0 : R) = 2 :=
+-- by test_polyrith
+--   "{\"data\":[\"(poly.const 1/1)\"],\"success\":true}"
+--   ["ff",
+--   "R",
+--   "0",
+--   "[(2 - 4)]",
+--   "(0 - 2)"]
+--   "linear_combination h"
 
+-- We comment the following tests so that we don't overwhelm the SageCell API.
 
 /-