Theorem IsTorsionFree.quotient_torsion

Modification history

2024-10-08 17:07

Mathlib/GroupTheory/Torsion.lean

feat: `IsTorsionFree ↔ NoZeroSMulDivisors` aliases (#17307) …

Deleted IsTorsionFree.quotient_torsion View on Github →

2023-05-25 22:41

Mathlib/GroupTheory/Torsion.lean

feat: port GroupTheory.Torsion (#4321)

Added IsTorsionFree.quotient_torsion View on Github →