Theorem Monoid.IsTorsionFree.subgroup

Modification history

2024-10-08 17:07

Mathlib/GroupTheory/Torsion.lean

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

Added Monoid.IsTorsionFree.subgroup View on Github →