Theorems · Definition · category theory
CategoryTheory.ShortComplex.SnakeInput.op
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Abelian C] →
CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex.SnakeInput CᵒᵖThe snake input in the opposite category that is deduced from a snake input.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Oppositestatement · cited by 8,081
- CategoryTheory.Abelianstatement and proof · cited by 1,753
- CategoryTheory.Equivalence.functorproof · cited by 1,268
- CategoryTheory.ShortComplex.SnakeInputstatement and proof · cited by 129
- CategoryTheory.ShortComplex.opproof · cited by 88
- CategoryTheory.ShortComplex.SnakeInput.L₂proof · cited by 71
- CategoryTheory.ShortComplex.SnakeInput.L₁proof · cited by 70
- CategoryTheory.ShortComplex.SnakeInput.L₀proof · cited by 69
- CategoryTheory.ShortComplex.SnakeInput.L₃proof · cited by 60
- CategoryTheory.ShortComplex.SnakeInput.v₁₂proof · cited by 47
- CategoryTheory.ShortComplex.SnakeInput.v₀₁proof · cited by 43
Cited by13
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.SnakeInput.L₂'_exactproof · cited by 3
- CategoryTheory.ShortComplex.SnakeInput.L₂'OpIsostatement · cited by 1
- CategoryTheory.ShortComplex.SnakeInput.L₃_exactproof · cited by 1
- CategoryTheory.ShortComplex.SnakeInput.P'IsoUnopOpPstatement · cited by 1
- CategoryTheory.ShortComplex.SnakeInput.PIsoUnopOpP'statement · cited by 1
- CategoryTheory.ShortComplex.SnakeInput.op_L₀statement and proof · cited by 0
- CategoryTheory.ShortComplex.SnakeInput.op_L₁statement and proof · cited by 0
- CategoryTheory.ShortComplex.SnakeInput.op_L₂statement and proof · cited by 0
- CategoryTheory.ShortComplex.SnakeInput.op_L₃statement and proof · cited by 0
- CategoryTheory.ShortComplex.SnakeInput.op_v₀₁statement and proof · cited by 0
- CategoryTheory.ShortComplex.SnakeInput.op_v₁₂statement and proof · cited by 0
- CategoryTheory.ShortComplex.SnakeInput.op_v₂₃statement and proof · cited by 0