Commit 2023-11-02 16:15 10702b58

View on Github →

feat: the snake lemma (#8084)

Estimated changes

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

added theorem CategoryTheory.ShortComplex.SnakeInput.L₀'_exact

added theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd

added theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁

added theorem CategoryTheory.ShortComplex.SnakeInput.L₀_exact

added theorem CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ

added theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_exact

added theorem CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁

added theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_exact

added theorem CategoryTheory.ShortComplex.SnakeInput.L₃_exact

added theorem CategoryTheory.ShortComplex.SnakeInput.op_δ

added theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ

added theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr

added theorem CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f

added theorem CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f