Theorem CategoryTheory.Abelian.isTorsionClass_iff_isTorsionFreeClass_op

Modification history

2026-10-20 23:05

Mathlib/CategoryTheory/Abelian/TorsionTheory/Basic.lean

feat(CategoryTheory/Abelian/TorsionTheory): Introduce torsion theory for abelian categories (#36744) …

Added CategoryTheory.Abelian.isTorsionClass_iff_isTorsionFreeClass_op View on Github →