Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-18 15:26 3a8e0a11

View on Github →

feat(group_theory/torsion): define the p-primary component of a group (#14312)

Estimated changes

Modified src/group_theory/order_of_element.lean

added theorem exists_order_of_eq_prime_pow_iff

Modified src/group_theory/torsion.lean

added theorem comm_group.primary_component.is_p_group

added def comm_group.primary_component

added def comm_group.torsion

added theorem comm_group.torsion_eq_torsion_submonoid

added theorem comm_monoid.primary_component.disjoint

added theorem comm_monoid.primary_component.exists_order_of_eq_prime_pow

added def comm_monoid.primary_component

modified theorem is_torsion_free.quotient_torsion

deleted def torsion

deleted theorem torsion_eq_torsion_submonoid