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