Theorem CategoryTheory.Abelian.isTorsionFreeClass_iff_isTorsionClass_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.isTorsionFreeClass_iff_isTorsionClass_op View on Github →