Commit 2025-05-14 07:47 753ef7e3

View on Github →

feat: more lemmas about torsion-free monoids (#24312) The new imports just come from making #min_imports and mk_iff available earlier. From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

Modified Mathlib/Algebra/Group/Torsion.lean

Modified Mathlib/Algebra/Lie/Weights/Chain.lean

Modified Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean

added theorem noZeroSMulDivisors_int_iff_isAddTorsionFree

added theorem noZeroSMulDivisors_nat_iff_isAddTorsionFree

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem isMulTorsionFree_iff_not_isOfFinOrder

added theorem not_isMulTorsionFree_iff_isOfFinOrder

added theorem not_isOfFinOrder_of_isMulTorsionFree

Modified Mathlib/GroupTheory/Torsion.lean

added theorem CommGroup.isMulTorsionFree_iff_torsion_eq_bot

added theorem not_isMulTorsionFree_of_isTorsion

added theorem not_isTorsion_of_isMulTorsionFree

Modified Mathlib/Topology/Instances/ZMultiples.lean