chore: remove outParam from IsCharP

2026-04-16 00:54:06 +00:00 · 2025-04-20 13:33:34 +10:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Grind/CommRing/Basic.lean
+++ b/src/Init/Grind/CommRing/Basic.lean
@@ -217,7 +217,7 @@ end CommRing

 open CommRing

-class IsCharP (α : Type u) [CommRing α] (p : outParam Nat) where
+class IsCharP (α : Type u) [CommRing α] (p : Nat) where
  ofNat_eq_zero_iff (p) : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0

 namespace IsCharP