Documentation

Mathlib.Algebra.Group.Torsion

Torsion-free monoids and groups #

This file defines torsion-free monoids as those monoids M for which n • · : M → M is injective for all non-zero natural number n.

TODO #

Replace Monoid.IsTorsionFree, which is mathematically incorrect for monoids which are not groups. This probably means we also want to get rid of NoZeroSMulDivisors, which is mathematically incorrect for the same reason.

source
class IsAddTorsionFree (M : Type u_1) [AddMonoid M] :
Prop

A monoid is R-torsion-free if scalar multiplication by every non-zero element a : R is injective.

Instances
    source
    theorem isAddTorsionFree_iff (M : Type u_1) [AddMonoid M] :
    IsAddTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun (a : M) => n • a
    source
    class IsMulTorsionFree (M : Type u_1) [Monoid M] :
    Prop

    A monoid is R-torsion-free if power by every non-zero element a : R is injective.

    Instances
      source
      theorem isMulTorsionFree_iff (M : Type u_1) [Monoid M] :
      IsMulTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun (a : M) => a ^ n
      source
      instance Subsingleton.to_isMulTorsionFree {M : Type u_1} [Monoid M] [Subsingleton M] :
      IsMulTorsionFree M
      source
      instance Subsingleton.to_isAddTorsionFree {M : Type u_1} [AddMonoid M] [Subsingleton M] :
      IsAddTorsionFree M
      source
      theorem pow_left_injective {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} (hn : n ≠ 0) :
      Function.Injective fun (a : M) => a ^ n
      source
      theorem nsmul_right_injective {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} (hn : n ≠ 0) :
      Function.Injective fun (a : M) => n • a
      source
      theorem pow_left_inj {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a b : M} (hn : n ≠ 0) :
      a ^ n = b ^ n ↔ a = b
      source
      theorem nsmul_right_inj {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a b : M} (hn : n ≠ 0) :
      n • a = n • b ↔ a = b
      source
      theorem zpow_left_injective {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} :
      n ≠ 0 → Function.Injective fun (a : G) => a ^ n
      source
      theorem zsmul_right_injective {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} :
      n ≠ 0 → Function.Injective fun (a : G) => n • a
      source
      theorem zpow_left_inj {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} {a b : G} (hn : n ≠ 0) :
      a ^ n = b ^ n ↔ a = b
      source
      theorem zsmul_right_inj {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a b : G} (hn : n ≠ 0) :
      n • a = n • b ↔ a = b
      source
      theorem zpow_eq_zpow_iff' {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} {a b : G} (hn : n ≠ 0) :
      a ^ n = b ^ n ↔ a = b

      Alias of zpow_left_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

      source
      theorem zsmul_eq_zsmul_iff' {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a b : G} (hn : n ≠ 0) :
      n • a = n • b ↔ a = b

      Alias of zsmul_right_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.