fix(init/algebra/group): use same definition for add_comm_monoid… (#177)

leanprover-community · Apr 7, 2020 · 4b0c279 · 4b0c279
1 parent a148f38
commit 4b0c279
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
@@ -212,7 +212,7 @@ class add_right_cancel_semigroup (α : Type u) extends add_semigroup α :=
 class add_monoid (α : Type u) extends add_semigroup α, has_zero α :=
 (zero_add : ∀ a : α, 0 + a = a) (add_zero : ∀ a : α, a + 0 = a)
 
-class add_comm_monoid (α : Type u) extends add_semigroup α, has_zero α, add_comm_semigroup α :=
+class add_comm_monoid (α : Type u) extends add_comm_semigroup α, has_zero α :=
 (zero_add : ∀ a : α, 0 + a = a)
 
 class add_group (α : Type u) extends add_semigroup α, has_zero α, has_neg α :=
@@ -472,4 +472,4 @@ by simp
 /- The following lemmas generate too many instances for rsimp -/
 attribute [no_rsimp]
   mul_assoc mul_comm mul_left_comm
-  add_assoc add_comm add_left_comm
+  add_assoc add_comm add_left_comm