Commit 2022-02-25 22:23 05d8188c

View on Github →

feat(group_theory/torsion): define torsion groups (#11850) I grepped for torsion group and didn't find anything -- hopefully adding this makes sense here.

Estimated changes

Modified src/group_theory/exponent.lean

modified theorem monoid.exponent_eq_zero_iff

added theorem monoid.exponent_exists_iff_ne_zero

Modified src/group_theory/order_of_element.lean

added theorem is_of_fin_order.quotient

added theorem is_of_fin_order_iff_coe

Created src/group_theory/torsion.lean

added theorem exponent_exists.is_torsion

added theorem is_torsion.exponent_exists

added theorem is_torsion.quotient_group

added theorem is_torsion.subgroup

added theorem is_torsion_of_fintype

added def monoid.is_torsion