Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 17:48 3fa09c27

View on Github →

feat(algebra/homology/homotopy): compatibilities of null_homotopic_map with composition and additive functors (#12392)

Estimated changes

Modified src/algebra/homology/homotopy.lean

added theorem homotopy.comp_null_homotopic_map'

added theorem homotopy.comp_null_homotopic_map

added theorem homotopy.map_null_homotopic_map'

added theorem homotopy.map_null_homotopic_map

added theorem homotopy.null_homotopic_map'_comp

modified theorem homotopy.null_homotopic_map'_f_eq_zero

added theorem homotopy.null_homotopic_map_comp

modified theorem homotopy.null_homotopic_map_f_eq_zero