Theorems · Theorem · category theory
CategoryTheory.ShortComplex.Exact.ab_finite
∀ {S : CategoryTheory.ShortComplex Ab}, S.Exact → ∀ [Finite ↑S.X₁] [Finite ↑S.X₃], Finite ↑S.X₂In an exact sequence of abelian groups, if the first and last groups are finite, then so is the middle one.
- Defined in
- Mathlib.Algebra.Homology.ShortComplex.Ab
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Equiv.symmproof · cited by 3,681
- AddSubgroupproof · cited by 3,232
- Finitestatement and proof · cited by 3,029
- HasQuotient.Quotientproof · cited by 2,301
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- CategoryTheory.ShortComplex.X₂statement and proof · cited by 1,115
- CategoryTheory.ShortComplex.X₁statement and proof · cited by 889
- CategoryTheory.ShortComplex.X₃statement and proof · cited by 876
- CategoryTheory.ShortComplex.gproof · cited by 658
- CategoryTheory.ShortComplex.fproof · cited by 653
- AddCommGrpCat.carrierstatement and proof · cited by 407
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.ShortComplex.ShortExact.ab_finite_iffproof · cited by 0