Commit 2023-04-17 21:44 6944050f

View on Github →

feat: port AlgebraicTopology.MooreComplex (#3467)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/MooreComplex.lean

added theorem AlgebraicTopology.NormalizedMooreComplex.d_squared

added def AlgebraicTopology.NormalizedMooreComplex.map

added def AlgebraicTopology.NormalizedMooreComplex.obj

added def AlgebraicTopology.NormalizedMooreComplex.objD

added def AlgebraicTopology.NormalizedMooreComplex.objX

added def AlgebraicTopology.normalizedMooreComplex

added theorem AlgebraicTopology.normalizedMooreComplex_objD