Theorem CategoryTheory.Abelian.IsTorsionFreeClass.torsionTheory

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.torsionTheoryView on Github →