Commit 2023-07-29 23:40 2471abe6

View on Github →

feat: forward port AlgebraicTopology.DoldKan.Compatibility (#6186) This PR is a forward port of mathlib3 PR !3#17923

Estimated changes

Modified Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean

added def AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq

added def AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso

added theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq

added def AlgebraicTopology.DoldKan.Compatibility.τ₀

added def AlgebraicTopology.DoldKan.Compatibility.τ₁

added def AlgebraicTopology.DoldKan.Compatibility.υ