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

Merge branch 'master' of github.com:fpvandoorn/Spectral

Browse source
This commit is contained in:
Yuri Sulyma 2017-06-07 09:40:08 -06:00
commit 9274ba04c9
2 changed files with 2 additions and 2 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)) :=
begin
apply dirsum_homotopy,
intro i y, esimp, exact sorry
intro i y, exact sorry
end
definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :

2
susp_product.hlean
View file

@ -1,5 +1,5 @@
import core
open susp smash pointed wedge prod
definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
sorry