chore(ring_theory/algebra): redefine module structure of Z-algebra in…

…stance (#1812) This redefines the Z-algebra instance, so that the module structure is definitionally equal to the Z-module structure of any `add_comm_group`
leanprover-community · Dec 18, 2019 · 5dae5d2 · 5dae5d2
1 parent bec46af
commit 5dae5d2
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean
@@ -574,7 +574,9 @@ def alg_hom_int
 
 /-- CRing ⥤ ℤ-Alg -/
 instance algebra_int : algebra ℤ R :=
-algebra.of_ring_hom coe $ by constructor; intros; simp
+{ to_fun := coe,
+  commutes' := λ _ _, mul_comm _ _,
+  smul_def' := λ _ _, gsmul_eq_mul _ _ }
 
 variables {R}
 /-- CRing ⥤ ℤ-Alg -/