Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 23:36 4d7683b2

View on Github →

feat(group_theory/torsion): torsion-free groups and quotients by torsion subgroups (#13173)

Estimated changes

Modified src/group_theory/torsion.lean

added theorem is_torsion.not_torsion_free

added theorem is_torsion_free.not_torsion

added theorem is_torsion_free.prod

added theorem is_torsion_free.quotient_torsion

added theorem is_torsion_free.subgroup

added def monoid.is_torsion_free

added theorem monoid.not_is_torsion_free_iff

added theorem monoid.not_is_torsion_iff