Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-08 21:44 e0b90625

View on Github →

doc(algebra/homology/homological_complex): fix doc and names (#15940) Some trivial modifications following #15690.

Estimated changes

Modified src/algebra/homology/homological_complex.lean

added def homological_complex.X_next_iso_self

deleted def homological_complex.X_next_iso_zero

added def homological_complex.X_prev_iso_self

added theorem homological_complex.X_prev_iso_self_comp_d_to

deleted def homological_complex.X_prev_iso_zero

deleted theorem homological_complex.X_prev_iso_zero_comp_d_to

added theorem homological_complex.d_from_comp_X_next_iso_self

deleted theorem homological_complex.d_from_comp_X_next_iso_zero