michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/algebra/category/morphism): remove sorry that was introduced by accident

Browse source
This commit is contained in:
Jeremy Avigad 2014-11-28 10:43:43 -05:00 committed by Leonardo de Moura
parent bb8d436e75
commit a9001166fd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/category/morphism.lean
View file

@ -54,7 +54,7 @@ namespace morphism
calc
g = g ∘ id : symm !id_right
... = g ∘ f ∘ g' : {symm Hr}
... = (g ∘ f) ∘ g' : sorry -- !assoc
... = (g ∘ f) ∘ g' : !assoc
... = id ∘ g' : {Hl}
... = g' : !id_left