Commit 2024-03-25 02:18 f7c6a4c6

View on Github →

chore: remove @[eqns] in Algebra/Homology/Homotopy (#11648)

Estimated changes

Modified Mathlib/Algebra/Homology/Homotopy.lean

modified theorem Homotopy.mkCoinductiveAux₂_add_one

modified theorem Homotopy.mkCoinductiveAux₂_zero

modified theorem Homotopy.mkInductiveAux₂_add_one

modified theorem Homotopy.mkInductiveAux₂_zero