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

Remove AddGroup symbol.

Browse source
This commit is contained in:
favonia 2017-06-08 17:48:26 -06:00
parent bc69a96faa
commit 8362498b56
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

@ -124,7 +124,7 @@ namespace group
dirsum_elim (λi, dirsum_incl Y' i ∘g f i) dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) : theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) := dirsum_functor f' ∘g dirsum_functor f ~ dirsum_functor (λi, f' i ∘g f i) :=
begin begin
apply dirsum_homotopy, apply dirsum_homotopy,
intro i y, reflexivity, intro i y, reflexivity,