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.

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

An additive monoid is torsion-free if scalar multiplication by every non-zero element a : ℕ is injective.

• nsmul_right_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => n • a

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

class IsMulTorsionFree (M : Type u_1) [Monoid M] : Prop

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

• pow_left_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Function.Injective fun (a : M) => a ^ n

theorem isMulTorsionFree_iff (M : Type u_1) [Monoid M] : IsMulTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun (a : M) => a ^ n

instance Subsingleton.to_isMulTorsionFree {M : Type u_1} [Monoid M] [Subsingleton M] : IsMulTorsionFree M

instance Subsingleton.to_isAddTorsionFree {M : Type u_1} [AddMonoid M] [Subsingleton M] : IsAddTorsionFree M

theorem pow_left_injective {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} (hn : n ≠ 0) : Function.Injective fun (a : M) => a ^ n

theorem nsmul_right_injective {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} (hn : n ≠ 0) : Function.Injective fun (a : M) => n • a

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

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

theorem zpow_left_injective {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} : n ≠ 0 → Function.Injective fun (a : G) => a ^ n

theorem zsmul_right_injective {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} : n ≠ 0 → Function.Injective fun (a : G) => n • a

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

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

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'.

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'.