Commit 2023-11-01 13:33 e896b09a

View on Github →

feat: introducing the input data of the snake lemma (#8081)

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down:

added theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up

added theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down

added theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up

added theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down

added theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up

added theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁

added theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂

added theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃

added theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁

added theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂

added theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃

added structure CategoryTheory.ShortComplex.SnakeInput