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

Remove useless esimp to speed up Lean.

Browse source
This commit is contained in:
favonia 2017-06-07 09:39:33 -06:00
parent df3ce3872f
commit 607e5343b1
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
algebra/direct_sum.hlean
View file

@ -114,7 +114,7 @@ namespace group
dirsum_functor (λi, homomorphism_mul (f i) (f' i)) := dirsum_functor (λi, homomorphism_mul (f i) (f' i)) :=
begin begin
apply dirsum_homotopy, apply dirsum_homotopy,
intro i y, esimp, exact sorry intro i y, exact sorry
end end
definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') : definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :