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

Fix the naming.

Browse source
This commit is contained in:
favonia 2017-06-08 18:06:59 -06:00
parent c0ea92a0b5
commit 56d97200d6
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

@ -156,7 +156,7 @@ namespace group
definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y := definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
dirsum_elim (λj, dirsum_incl Y (f j)) dirsum_elim (λj, dirsum_incl Y (f j))
definition dirsum_functor_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' := definition dirsum_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' :=
let to_hom := dirsum_functor (λ i, f i) in let to_hom := dirsum_functor (λ i, f i) in
let from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in let from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in
begin begin