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 IsMulTorsionFree.pow_right_injective {M : Type u_1} [CancelMonoid M] [IsMulTorsionFree M] {a : M} (ha : a ≠ 1) : Function.Injective fun (n : ℕ) => a ^ n

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

theorem IsMulTorsionFree.pow_right_injective_iff {M : Type u_1} [CancelMonoid M] [IsMulTorsionFree M] {a : M} : (Function.Injective fun (n : ℕ) => a ^ n) ↔ a ≠ 1

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

@[simp]

theorem IsMulTorsionFree.pow_right_inj {M : Type u_1} [CancelMonoid M] [IsMulTorsionFree M] {a : M} (ha : a ≠ 1) {n m : ℕ} : a ^ n = a ^ m ↔ n = m

@[simp]

theorem IsAddTorsionFree.nsmul_left_inj {M : Type u_1} [AddCancelMonoid M] [IsAddTorsionFree M] {a : M} (ha : a ≠ 0) {n m : ℕ} : n • a = m • a ↔ n = m

theorem IsMulTorsionFree.hasUniqueRoots {M : Type u_1} [CommMonoid M] [IsMulTorsionFree M] : HasUniqueRoots M

A commutative torsion-free monoid has unique roots.

This is not an instance, to avoid an expensive instance loop with HasUniqueRoots M → IsMulTorsionFree M.

theorem IsAddTorsionFree.hasUniqueDiv {M : Type u_1} [AddCommMonoid M] [IsAddTorsionFree M] : HasUniqueDiv M

A commutative torsion-free additive monoid has unique divisibility.

This is not an instance, to avoid an expensive instance loop with HasUniqueDiv M → IsAddTorsionFree M.

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 IsMulTorsionFree.zpow_right_injective_iff {G : Type u_2} [Group G] {a : G} [IsMulTorsionFree G] : (Function.Injective fun (x : ℤ) => a ^ x) ↔ a ≠ 1

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

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

Alias of the reverse direction of IsMulTorsionFree.zpow_right_injective_iff.

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

Alias of the reverse direction of IsAddTorsionFree.zsmul_left_injective_iff.

@[simp]

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

@[simp]

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

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.