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 instNoNatZeroDivisorsOfHasUniqueDiv {M : Type u_1} [AddCommMonoid M] [HasUniqueDiv M] : Lean.Grind.NoNatZeroDivisors M

instance instHasUniqueRootsOfSubsingleton {M : Type u_1} [Monoid M] [Subsingleton M] : HasUniqueRoots M

instance insthasUniqueDivOfSubsingleton {M : Type u_1} [AddMonoid M] [Subsingleton M] : HasUniqueDiv M

theorem Commute.eq_of_pow_eq_pow {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a b : M} (hab : Commute a b) (hn : n ≠ 0) (habn : a ^ n = b ^ n) : a = b

theorem AddCommute.eq_of_nsmul_eq_nsmul {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a b : M} (hab : AddCommute a b) (hn : n ≠ 0) (habn : n • a = n • b) : a = b

theorem Commute.pow_left_inj {M : Type u_1} [Monoid M] [IsMulTorsionFree M] {n : ℕ} {a b : M} (hab : Commute a b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem AddCommute.nsmul_right_inj {M : Type u_1} [AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a b : M} (hab : AddCommute a b) (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

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

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

theorem Commute.eq_of_zpow_eq_zpow {G : Type u_2} [Group G] {n : ℤ} {a b : G} [IsMulTorsionFree G] (hab : Commute a b) (hn : n ≠ 0) (habn : a ^ n = b ^ n) : a = b

theorem AddCommute.eq_of_zsmul_eq_zsmul {G : Type u_2} [AddGroup G] {n : ℤ} {a b : G} [IsAddTorsionFree G] (hab : AddCommute a b) (hn : n ≠ 0) (habn : n • a = n • b) : a = b

theorem Commute.zpow_left_inj {G : Type u_2} [Group G] {n : ℤ} {a b : G} [IsMulTorsionFree G] (hab : Commute a b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

theorem isSelfInv_iff_eq_one {G : Type u_2} [Group G] {a : G} [IsMulTorsionFree G] : IsSelfInv a ↔ a = 1

theorem isSelfNeg_iff_eq_zero {G : Type u_2} [AddGroup G] {a : G} [IsAddTorsionFree G] : IsSelfNeg a ↔ a = 0

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

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

theorem zpow_left_inj {G : Type u_2} [Group G] [HasUniqueRoots G] {n : ℤ} {a b : G} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

theorem zsmul_right_inj {G : Type u_2} [AddGroup G] [HasUniqueDiv G] {n : ℤ} {a b : G} (hn : n ≠ 0) : n • a = n • b ↔ a = b

@[deprecated zpow_left_inj (since := "2026-09-30")]

theorem zpow_eq_zpow_iff' {G : Type u_2} [Group G] [HasUniqueRoots G] {n : ℤ} {a b : G} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b

Alias of zpow_left_inj.

@[deprecated zsmul_right_inj (since := "2026-09-30")]

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

Alias of zsmul_right_inj.