Commit 2023-04-21 04:55 aca58344

View on Github →

feat: port AlgebraicTopology.DoldKan.Decomposition (#3544)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean

added def AlgebraicTopology.DoldKan.MorphComponents.id

added theorem AlgebraicTopology.DoldKan.MorphComponents.id_φ

added def AlgebraicTopology.DoldKan.MorphComponents.postComp

added theorem AlgebraicTopology.DoldKan.MorphComponents.postComp_φ

added def AlgebraicTopology.DoldKan.MorphComponents.preComp

added theorem AlgebraicTopology.DoldKan.MorphComponents.preComp_φ

added def AlgebraicTopology.DoldKan.MorphComponents.φ

added structure AlgebraicTopology.DoldKan.MorphComponents

added theorem AlgebraicTopology.DoldKan.decomposition_Q