test(fields): extend Mersenne31 regression coverage

tests/CompPolyTests.lean

@@ -33,6 +33,7 @@ public import CompPolyTests.Fields.Extension.Arithmetic
 public import CompPolyTests.Fields.Extension.Binomial
 public import CompPolyTests.Fields.KoalaBear.Fast
 public import CompPolyTests.Fields.Mersenne31.Fast
+public import CompPolyTests.Fields.Mersenne31.Instances
 public import CompPolyTests.Fields.PrattCertificate
 public import CompPolyTests.LinearAlgebra.Dense
 public import CompPolyTests.Multilinear.Equiv

tests/CompPolyTests/Fields/Mersenne31/Fast.lean

@@ -40,5 +40,7 @@ namespace Mersenne31.Fast
 #guard toNat ((37 : Field) / 37) = 1
 #guard toField ((37 : Field)⁻¹) = ((37 : Mersenne31.Field)⁻¹)
 #guard toField ((37 : Field) ^ (-3 : Int)) = ((37 : Mersenne31.Field) ^ (-3 : Int))
+#guard ringEquiv ((123 : Field) + 456) = ((123 : Mersenne31.Field) + 456)
+#guard ringEquiv ((123 : Field) * 456) = ((123 : Mersenne31.Field) * 456)
 
 end Mersenne31.Fast

tests/CompPolyTests/Fields/Mersenne31/Instances.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adrien Lacombe
+-/
+module
+
+public import CompPoly.Fields.Mersenne31.Fast
+
+/-!
+# Mersenne31 Field Instance Tests
+
+Regression checks for the canonical and fast Mersenne31 field instances.
+-/
+
+public section
+
+namespace Mersenne31
+
+example : Fact (Nat.Prime fieldSize) := inferInstance
+
+example : _root_.Field Field := inferInstance
+
+example : NonBinaryField Field := inferInstance
+
+example : (2 : Field) ≠ 0 := by
+  exact NonBinaryField.char_neq_2
+
+end Mersenne31
+
+namespace Mersenne31.Fast
+
+example : _root_.Field Field := inferInstance
+
+example : NonBinaryField Field := inferInstance
+
+end Mersenne31.Fast