Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-29 18:28 13ff898b

View on Github →

refactor(algebra/homology): better defeqs, less case splitting (#15690)

Estimated changes

Modified src/algebra/homology/additive.lean

Modified src/algebra/homology/complex_shape.lean

modified def complex_shape.next

added theorem complex_shape.next_eq'

deleted theorem complex_shape.next_eq_some

modified def complex_shape.prev

added theorem complex_shape.prev_eq'

deleted theorem complex_shape.prev_eq_some

Modified src/algebra/homology/homological_complex.lean

modified def homological_complex.X_next

modified def homological_complex.X_next_iso_zero

modified def homological_complex.X_prev

modified def homological_complex.X_prev_iso_zero

modified theorem homological_complex.X_prev_iso_zero_comp_d_to

modified def homological_complex.d_from

modified theorem homological_complex.d_from_comp_X_next_iso_zero

modified theorem homological_complex.d_from_eq_zero

modified def homological_complex.d_to

modified theorem homological_complex.d_to_eq_zero

modified def homological_complex.hom.next

modified def homological_complex.hom.prev

modified theorem homological_complex.hom.sq_from_id

Modified src/algebra/homology/homology.lean

modified theorem homological_complex.boundaries_eq_bot

modified theorem homological_complex.cycles_eq_top

Modified src/algebra/homology/homotopy.lean

modified theorem d_next_eq_d_from_from_next

modified def from_next

modified theorem homotopy.mk_coinductive_aux₃

modified theorem homotopy.mk_inductive_aux₃

modified theorem prev_d_eq_to_prev_d_to

modified def to_prev

Modified src/algebra/homology/homotopy_category.lean

Modified src/category_theory/functor/left_derived.lean