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]
:
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
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_eq_zpow_iff'
{G : Type u_2}
[Group G]
[IsMulTorsionFree G]
{n : ℤ}
{a b : G}
(hn : n ≠ 0)
:
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)
:
Alias of zsmul_right_inj, for ease of discovery alongside zsmul_le_zsmul_iff'
and zsmul_lt_zsmul_iff'.