feat: add LawfulOfScientific class

src/Init/Grind/Ring.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Init.Grind.Ring.Basic
 public import Init.Grind.Ring.Field
+public import Init.Grind.Ring.OfScientific
 public import Init.Grind.Ring.Envelope
 public import Init.Grind.Ring.CommSolver
 public import Init.Grind.Ring.CommSemiringAdapter

src/Init/Grind/Ring/OfScientific.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Init.Grind.Ring.Field
+public import Init.Data.OfScientific
+
+public section
+
+namespace Lean.Grind
+
+attribute [local instance] Semiring.natCast
+
+/--
+A type class that ensures that `OfScientific.ofScientific` is properly defined with respect to
+the field structure.
+-/
+class LawfulOfScientific (α : Type u) [Field α] [OfScientific α] : Prop where
+  /--
+  `OfScientific.ofScientific` is properly defined with respect to the field structure.
+  -/
+  ofScientific_def :
+    OfScientific.ofScientific m s e = if s then (Nat.cast m : α) / 10^e else (Nat.cast m : α) * 10^e
+
+end Lean.Grind

src/Init/GrindInstances/Ring/Rat.lean

@@ -6,7 +6,7 @@ Authors: Robin Arnez
 module
 
 prelude
-public import Init.Grind.Ring.Field
+public import Init.Grind.Ring.OfScientific
 public import Init.Data.Rat.Lemmas
 
 public section
@@ -56,4 +56,7 @@ instance : NoNatZeroDivisors Rat where
     change k * a = k * b at h₂
     simpa [← Rat.mul_assoc, Rat.inv_mul_cancel, h₁] using congrArg ((k : Rat)⁻¹ * ·) h₂
 
+instance : LawfulOfScientific Rat where
+  ofScientific_def {m s e} := by rw [Rat.ofScientific_def_eq_if]
+
 end Lean.Grind