Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 04c4abf

Browse files
ChrisHughes24johoelzl
authored andcommitted
fix(algebra/group): fix bit0_zero to use (0 : alpha) not (0 : nat)
1 parent 39bab47 commit 04c4abf

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

algebra/group.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -499,8 +499,9 @@ instance [add_comm_group α] : comm_group (multiplicative α) :=
499499
section add_monoid
500500
variables [add_monoid α] {a b c : α}
501501

502-
@[simp] lemma bit0_zero : bit0 0 = 0 := add_zero _
503-
@[simp] lemma bit1_zero : bit1 0 = 1 := add_zero _
502+
@[simp] lemma bit0_zero : bit0 (0 : α) = 0 := add_zero _
503+
@[simp] lemma bit1_zero [has_one α] : bit1 (0 : α) = 1 := by simp [bit1]
504+
504505
end add_monoid
505506

506507
section add_group

0 commit comments

Comments
 (0)