fix(algebra/group): fix bit0_zero to use (0 : alpha) not (0 : nat)

leanprover-community · Sep 15, 2018 · 04c4abf · 04c4abf
1 parent 39bab47
commit 04c4abf
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/algebra/group.lean b/algebra/group.lean
@@ -499,8 +499,9 @@ instance [add_comm_group α] : comm_group (multiplicative α) :=
 section add_monoid
   variables [add_monoid α] {a b c : α}
 
-  @[simp] lemma bit0_zero : bit0 0 = 0 := add_zero _
-  @[simp] lemma bit1_zero : bit1 0 = 1 := add_zero _
+  @[simp] lemma bit0_zero : bit0 (0 : α) = 0 := add_zero _
+  @[simp] lemma bit1_zero [has_one α] : bit1 (0 : α) = 1 := by simp [bit1]
+
 end add_monoid
 
 section add_group