Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-05-09 02:37
1e8f3817
View on Github →
feat(algebraic_topology/dold_kan): defining some null homotopic maps (
#13085
)
Estimated changes
Modified
docs/references.bib
Modified
src/algebra/homology/complex_shape.lean
added
theorem
complex_shape.down'_mk
added
theorem
complex_shape.down_mk
Created
src/algebraic_topology/dold_kan/homotopies.lean
added
def
algebraic_topology.dold_kan.Hσ
added
theorem
algebraic_topology.dold_kan.Hσ_eq_zero
added
def
algebraic_topology.dold_kan.c
added
theorem
algebraic_topology.dold_kan.c_mk
added
theorem
algebraic_topology.dold_kan.cs_down_0_not_rel_left
added
def
algebraic_topology.dold_kan.homotopy_Hσ_to_zero
added
def
algebraic_topology.dold_kan.hσ'
added
theorem
algebraic_topology.dold_kan.hσ'_eq
added
theorem
algebraic_topology.dold_kan.hσ'_eq_zero
added
theorem
algebraic_topology.dold_kan.hσ'_naturality
added
def
algebraic_topology.dold_kan.hσ
added
theorem
algebraic_topology.dold_kan.map_Hσ
added
theorem
algebraic_topology.dold_kan.map_hσ'
added
def
algebraic_topology.dold_kan.nat_trans_Hσ
Created
src/algebraic_topology/dold_kan/notations.lean