Mathlib Changelog
Changelog
About
Github
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