Commit 2021-05-17 12:38 d201a182

View on Github →

refactor(algebra/homology/homotopy): avoid needing has_zero_object (#7621) A refactor of the definition of homotopy, so we don't need has_zero_object.

Estimated changes

Modified src/algebra/homology/homotopy.lean

added def d_next

added theorem d_next_comp_left

added theorem d_next_comp_right

added theorem d_next_eq

added theorem d_next_eq_d_from_from_next

deleted def from_next'

deleted theorem from_next'_add

deleted theorem from_next'_comp_left

deleted theorem from_next'_comp_right

deleted theorem from_next'_eq

deleted theorem from_next'_neg

deleted theorem from_next'_zero

added def from_next

deleted theorem homotopy.comm

added theorem homotopy.d_next_succ_chain_complex

added theorem homotopy.d_next_zero_chain_complex

deleted theorem homotopy.from_next'_succ_chain_complex

deleted theorem homotopy.from_next'_zero_chain_complex

deleted def homotopy.from_next

added theorem homotopy.prev_d_chain_complex

deleted theorem homotopy.to_prev'_chain_complex

deleted def homotopy.to_prev

added def prev_d

added theorem prev_d_comp_left

added theorem prev_d_eq

added theorem prev_d_eq_to_prev_d_to

deleted def to_prev'

deleted theorem to_prev'_add

deleted theorem to_prev'_comp_left

deleted theorem to_prev'_eq

deleted theorem to_prev'_neg

deleted theorem to_prev'_zero

added def to_prev