From f93fc153d4b2765af3b742d0b1faafa4609b743a Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 9 Jun 2017 14:28:52 -0400 Subject: [PATCH] fix explicit arguments of dirsum_functor_homotopy --- algebra/graded.hlean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index a34dd62..ee6c7bd 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -391,14 +391,14 @@ dirsum_functor (λi, smul_homomorphism (N i) r) definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) : dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n := begin - refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_mul⁻¹, + refine dirsum_functor_homotopy _ _ _ n ⬝ !dirsum_functor_mul⁻¹, intro i ni, exact to_smul_right_distrib r s ni end definition dirsum_mul_smul' (r s : R) (n : dirsum' N) : dirsum_smul (r * s) n = (dirsum_smul r ∘a dirsum_smul s) n := begin - refine dirsum_functor_homotopy _ n ⬝ (dirsum_functor_compose _ _ n)⁻¹ᵖ, + refine dirsum_functor_homotopy _ _ _ n ⬝ (dirsum_functor_compose _ _ n)⁻¹ᵖ, intro i ni, exact to_mul_smul r s ni end @@ -408,7 +408,7 @@ proof dirsum_mul_smul' r s n qed definition dirsum_one_smul (n : dirsum' N) : dirsum_smul 1 n = n := begin - refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_gid, + refine dirsum_functor_homotopy _ _ _ n ⬝ !dirsum_functor_gid, intro i ni, exact to_one_smul ni end