Commit 2023-05-25 22:41 fa76ef04

View on Github →

feat: port GroupTheory.Torsion (#4321)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Torsion.lean

added theorem AddMonoid.IsTorsion.module_of_finite

added theorem AddMonoid.IsTorsion.module_of_torsion

added theorem CommGroup.primaryComponent.isPGroup

added def CommGroup.primaryComponent

added def CommGroup.torsion

added theorem CommGroup.torsion_eq_torsion_submonoid

added theorem CommMonoid.primaryComponent.disjoint

added theorem CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow

added def CommMonoid.primaryComponent

added theorem CommMonoid.torsion.isTorsion

added def CommMonoid.torsion

added theorem ExponentExists.isTorsion

added theorem IsTorsion.exponentExists

added theorem IsTorsion.extension_closed

added theorem IsTorsion.not_torsion_free

added theorem IsTorsion.of_surjective

added theorem IsTorsion.quotient_iff

added theorem IsTorsion.subgroup

added theorem IsTorsionFree.not_torsion

added theorem IsTorsionFree.prod

added theorem IsTorsionFree.quotient_torsion

added theorem IsTorsionFree.subgroup

added def Monoid.IsTorsion.torsionMulEquiv

added theorem Monoid.IsTorsion.torsionMulEquiv_apply

added theorem Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe

added theorem Monoid.IsTorsion.torsion_eq_top

added def Monoid.IsTorsion

added def Monoid.IsTorsionFree

added theorem Monoid.not_isTorsionFree_iff

added theorem Monoid.not_isTorsion_iff

added def Torsion.ofTorsion

added theorem isTorsion_of_finite