fix

eric-wieser · eric-wieser · commit c85d804b5a31 · 2024-03-08T21:52:14.000Z
diff --git a/Counterexamples/Monic_nonRegular.lean b/Counterexamples/Monic_nonRegular.lean
@@ -60,7 +60,6 @@ instance : CommMonoid N₃ where
   mul_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
   one_mul := by rintro ⟨⟩ <;> rfl
   mul_one := by rintro ⟨⟩ <;> rfl
-  nsmul := nsmulRec
   mul_comm := by rintro ⟨⟩ ⟨⟩ <;> rfl
 
 instance : CommSemiring N₃ :=
@@ -72,7 +71,8 @@ instance : CommSemiring N₃ :=
     left_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
     right_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
     zero_mul := by rintro ⟨⟩ <;> rfl
-    mul_zero := by rintro ⟨⟩ <;> rfl }
+    mul_zero := by rintro ⟨⟩ <;> rfl
+    nsmul := nsmulRec }
 
 theorem X_add_two_mul_X_add_two : (X + C 2 : N₃[X]) * (X + C 2) = (X + C 2) * (X + C 3) := by
   simp only [mul_add, add_mul, X_mul, add_assoc]
