max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/algebra.lean): avoid use of mul in translating additive to multiplicative

Browse source
This commit is contained in:
Jeremy Avigad 2016-11-14 15:06:50 -05:00 • committed by Leonardo de Moura
parent d5aa92eaeb
commit f20fe53dd2
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/algebra.lean
View file

@ -88,11 +88,11 @@ group.mul_left_inv
@[class] def add_comm_group := comm_group
instance add_semigroup.to_has_add {A : Type u} [s : add_semigroup A] : has_add A :=
⟨@mul A (@semigroup.to_has_mul A s)⟩
⟨@semigroup.mul A s⟩
instance add_monoid.to_has_zero {A : Type u} [s : add_monoid A] : has_zero A :=
⟨@one A (@monoid.to_has_one A s)⟩
⟨@monoid.one A s⟩
instance add_group.to_has_neg {A : Type u} [s : add_group A] : has_neg A :=
⟨@inv A (@group.to_has_inv A s)⟩
⟨@group.inv A s⟩
meta def multiplicative_to_additive : name_map name :=
rb_map.of_list $