chore(Algebra/Homology/ShortComplex/SnakeLemma): fix typo Functor₉ …

…-> `Functor₀` (#13114)
leanprover-community · May 22, 2024 · 0df2dd3 · 0df2dd3
1 parent f485750
commit 0df2dd3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@@ -446,7 +446,7 @@ end
 
 /-- The functor which sends `S : SnakeInput C` to its zeroth line `S.L₀`. -/
 @[simps]
-def functorL₉ : SnakeInput C ⥤ ShortComplex C where
+def functorL₀ : SnakeInput C ⥤ ShortComplex C where
   obj S := S.L₀
   map f := f.f₀