Torsion-free monoids and groups #

This file proves lemmas about torsion-free monoids. A monoid M is torsion-free if n • · : M → M is injective for all non-zero natural numbers n.

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

Documentation

Mathlib.Algebra.Group.Torsion

Torsion-free monoids and groups #