Theorem IsTorsion.extension_closed

Modification history

2026-07-24 18:27

Mathlib/GroupTheory/Torsion.lean

chore(GroupTheory/Torsion): rename `IsTorsion` to `IsMulTorsion` (#41213) …

Deleted IsTorsion.extension_closed View on Github →

2023-05-25 22:41

Mathlib/GroupTheory/Torsion.lean

feat: port GroupTheory.Torsion (#4321)

Added IsTorsion.extension_closed View on Github →