Theorem CategoryTheory.Abelian.TorsionTheory.isTorsionClass

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