Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-31 14:15 2e8ebdc0

View on Github →

feat(algebra/homology): Construction of null homotopic chain complex … (#11125) …morphisms and one lemma on addivity of homotopies

Estimated changes

Modified src/algebra/homology/homotopy.lean

added def homotopy.add

added def homotopy.null_homotopic_map'

added theorem homotopy.null_homotopic_map'_f

added theorem homotopy.null_homotopic_map'_f_eq_zero

added theorem homotopy.null_homotopic_map'_f_of_not_rel_left

added theorem homotopy.null_homotopic_map'_f_of_not_rel_right

added def homotopy.null_homotopic_map

added theorem homotopy.null_homotopic_map_f

added theorem homotopy.null_homotopic_map_f_eq_zero

added theorem homotopy.null_homotopic_map_f_of_not_rel_left

added theorem homotopy.null_homotopic_map_f_of_not_rel_right

added def homotopy.null_homotopy'

added def homotopy.null_homotopy