fix(data/zmod/algebra): fix

Author: eric-wieser

src/data/zmod/algebra.lean

@@ -21,6 +21,7 @@ variables {n : ℕ} (m : ℕ) [char_p R m]
 /-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
 def algebra' (h : m ∣ n) : algebra (zmod n) R :=
 { smul := λ a r, a * r,
+  to_opposite_has_scalar := { smul := λ a r, r * a },
   commutes' := λ a r, show (a * r : R) = r * a,
   begin
     rcases zmod.int_cast_surjective a with ⟨k, rfl⟩,
@@ -29,6 +30,7 @@ def algebra' (h : m ∣ n) : algebra (zmod n) R :=
     exact commute.cast_int_left r k,
   end,
   smul_def' := λ a r, rfl,
+  op_smul_def' := λ r a, rfl,
   .. zmod.cast_hom h R }
 
 end