feat: IsCharP instance for Semiring envelope

src/Init/Grind/Ring/Envelope.lean

@@ -316,6 +316,26 @@ instance [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDiv
     replace h₂ := NoNatZeroDivisors.no_nat_zero_divisors k (a₁ + b₂) (a₂ + b₁) h₁ h₂
     apply Quot.sound; simp [r]; exists 0; simp [h₂]
 
+instance {p} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (OfSemiring.Q α) p where
+  ofNat_ext_iff := by
+    intro x y
+    constructor
+    next =>
+      intro h
+      replace h : natCast x = natCast y := h; simp at h
+      replace h := Q.exact h; simp [r] at h
+      rcases h with ⟨k, h⟩
+      replace h : OfNat.ofNat (α := α) x = OfNat.ofNat y := by
+        replace h := AddRightCancel.add_right_cancel _ _ _ h
+        simp [Semiring.ofNat_eq_natCast, h]
+      have := IsCharP.ofNat_ext_iff p |>.mp h
+      simp at this; assumption
+    next =>
+      intro h
+      have := IsCharP.ofNat_ext_iff (α := α) p |>.mpr h
+      apply Quot.sound
+      exists 0; simp [← Semiring.ofNat_eq_natCast, this]
+
 end OfSemiring
 end Lean.Grind.Ring