feat(algebra/homology): homotopies between chain maps (#7483)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · May 15, 2021 · c63caeb · c63caeb
1 parent cc47aff
commit c63caeb
Show file tree

Hide file tree

Showing 2 changed files with 500 additions and 1 deletion.
diff --git a/src/algebra/homology/additive.lean b/src/algebra/homology/additive.lean
@@ -41,7 +41,6 @@ instance : has_sub (C ⟶ D) := ⟨λ f g, { f := λ i, f.f i - g.f i, }⟩
 @[simp] lemma neg_f_apply (f : C ⟶ D) (i : ι) : (-f).f i = -(f.f i) := rfl
 @[simp] lemma sub_f_apply (f g : C ⟶ D) (i : ι) : (f - g).f i = f.f i - g.f i := rfl
 
-
 /- TODO(jmc/Scott): the instance below doesn't have the correct defeq for `nsmul` and `gsmul`.
 We should generalize `function.injective.add_comm_group` and friends.
 For the `R`-linear version, it will be very convenient to have