From 56d97200d63dccac6d1cee238884c2cbcb0bb982 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 18:06:59 -0600 Subject: [PATCH] Fix the naming. --- algebra/direct_sum.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index aeb3142..b21ccd3 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -156,7 +156,7 @@ namespace group definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y := 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 from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in begin