From 04c4abf13e75e254265313dd63678209ce40d90d Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+dorhinj@users.noreply.github.com>
Date: Sat, 15 Sep 2018 13:19:07 +0100
Subject: [PATCH] fix(algebra/group): fix bit0_zero to use (0 : alpha) not (0 :
 nat)

---
 algebra/group.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/algebra/group.lean b/algebra/group.lean
index e7ed905b484cd..092a3ebab7794 100644
--- 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