Theorem IsMulTorsionFree.hasUniqueRoots

Modification history

2026-10-17 18:35
Mathlib/Algebra/Group/Torsion.lean
feat: add QuotientGroup.instHasUniqueRoots (#44838) …
Added IsMulTorsionFree.hasUniqueRootsView on Github →