Commit 2024-05-22 14:18 0df2dd35

View on Github →

chore(Algebra/Homology/ShortComplex/SnakeLemma): fix typo Functor₉ -> Functor₀ (#13114)

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

added def CategoryTheory.ShortComplex.SnakeInput.functorL₀

deleted def CategoryTheory.ShortComplex.SnakeInput.functorL₉