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.

instance instNoNatZeroDivisorsOfIsAddTorsionFree {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] : Lean.Grind.NoNatZeroDivisors M

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 pow_eq_one_iff_left {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M} (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1

theorem nsmul_eq_zero_iff_right {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M} (hn : n ≠ 0) : n • a = 0 ↔ a = 0

@[simp]

theorem pow_eq_one_iff {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M} : a ^ n = 1 ↔ a = 1 ∨ n = 0

@[simp]

theorem nsmul_eq_zero_iff {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M} : n • a = 0 ↔ a = 0 ∨ n = 0

theorem pow_eq_one_iff_right {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M} (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0

theorem nsmul_eq_zero_iff_left {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M} (ha : a ≠ 0) : n • a = 0 ↔ n = 0

@[deprecated nsmul_eq_zero_iff_left (since := "2025-10-19")]

theorem IsAddTorsionFree.nsmul_eq_zero_iff' {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M} (ha : a ≠ 0) : n • a = 0 ↔ n = 0

Alias of nsmul_eq_zero_iff_left.

@[deprecated pow_eq_one_iff_right (since := "2025-10-19")]

theorem IsMulTorsionFree.pow_eq_one_iff' {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M} (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0

Alias of pow_eq_one_iff_right.

theorem sq_eq_one {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {a : M} : a ^ 2 = 1 ↔ a = 1

See sq_eq_one_iff for a version that holds in rings.

theorem two_nsmul_eq_zero {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {a : M} : 2 • a = 0 ↔ a = 0

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

theorem IsMulTorsionFree.zpow_eq_one_iff_left {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} {a : G} (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1

theorem IsAddTorsionFree.zsmul_eq_zero_iff_right {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a : G} (hn : n ≠ 0) : n • a = 0 ↔ a = 0

@[simp]

theorem IsMulTorsionFree.zpow_eq_one_iff {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} {a : G} : a ^ n = 1 ↔ a = 1 ∨ n = 0

@[simp]

theorem IsAddTorsionFree.zsmul_eq_zero_iff {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a : G} : n • a = 0 ↔ a = 0 ∨ n = 0

theorem IsMulTorsionFree.zpow_eq_one_iff_right {G : Type u_2} [Group G] [IsMulTorsionFree G] {n : ℤ} {a : G} (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0

theorem IsAddTorsionFree.zsmul_eq_zero_iff_left {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a : G} (ha : a ≠ 0) : n • a = 0 ↔ n = 0

theorem self_eq_inv {G : Type u_2} [Group G] [IsMulTorsionFree G] {a : G} : a = a⁻¹ ↔ a = 1

theorem self_eq_neg {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {a : G} : a = -a ↔ a = 0

theorem inv_eq_self {G : Type u_2} [Group G] [IsMulTorsionFree G] {a : G} : a⁻¹ = a ↔ a = 1

theorem neg_eq_self {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {a : G} : -a = a ↔ a = 0

theorem self_ne_inv {G : Type u_2} [Group G] [IsMulTorsionFree G] {a : G} : a ≠ a⁻¹ ↔ a ≠ 1

theorem self_ne_neg {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {a : G} : a ≠ -a ↔ a ≠ 0

theorem inv_ne_self {G : Type u_2} [Group G] [IsMulTorsionFree G] {a : G} : a⁻¹ ≠ a ↔ a ≠ 1

theorem neg_ne_self {G : Type u_2} [AddGroup G] [IsAddTorsionFree G] {a : G} : -a ≠ a ↔ a ≠ 0