Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:09 cf3b996e

View on Github →

feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172) Co-authored by: Alex J. Best alex.j.best@gmail.com

Estimated changes

Modified src/group_theory/order_of_element.lean

added theorem is_of_fin_order.apply

deleted theorem is_of_fin_order.quotient

modified theorem is_of_fin_order_iff_coe

added theorem monoid_hom.is_of_fin_order

Modified src/group_theory/torsion.lean

added theorem add_monoid.is_torsion.module_of_fintype

added theorem add_monoid.is_torsion.module_of_torsion

modified theorem exponent_exists.is_torsion

added theorem is_torsion.extension_closed

added theorem is_torsion.of_surjective

deleted theorem is_torsion.quotient_group

added theorem is_torsion.quotient_iff