doc-next-gen

Mathlib.Algebra.Group.Torsion

Module docstring

{"# Torsion-free monoids and groups

This file defines torsion-free monoids as those monoids M for which n • · : M → M is injective for all non-zero natural number n.

TODO

Replace Monoid.IsTorsionFree, which is mathematically incorrect for monoids which are not groups. This probably means we also want to get rid of NoZeroSMulDivisors, which is mathematically incorrect for the same reason. "}

IsAddTorsionFree structure
[AddMonoid M]
Full source 
/-- A monoid is `R`-torsion-free if scalar multiplication by every non-zero element `a : R` is
injective. -/
@[mk_iff]
class IsAddTorsionFree [AddMonoid M] where
  protected nsmul_right_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Injective fun a : M ↦ n • a
Torsion-free additive monoid
Informal description
An additive monoid \( M \) is called *torsion-free* if for every nonzero natural number \( n \), the function \( x \mapsto n \cdot x \) is injective on \( M \). Equivalently, for any \( x, y \in M \) and nonzero \( n \), we have \( n \cdot x = n \cdot y \) if and only if \( x = y \).
IsMulTorsionFree structure
Full source 
/-- A monoid is `R`-torsion-free if power by every non-zero element `a : R` is injective. -/
@[to_additive, mk_iff]
class IsMulTorsionFree where
  protected pow_left_injective ⦃n : ℕ⦄ (hn : n ≠ 0) : Injective fun a : M ↦ a ^ n
Multiplicatively torsion-free monoid
Informal description
A monoid $M$ is called *multiplicatively torsion-free* if for every nonzero natural number $n$, the $n$-th power function $a \mapsto a^n$ is injective on $M$. Equivalently, for any $a, b \in M$ and nonzero $n$, we have $a^n = b^n$ if and only if $a = b$.
pow_left_inj theorem
(hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b
Full source 
@[to_additive nsmul_right_inj]
lemma pow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (pow_left_injective hn).eq_iff
Power Equality Criterion in Torsion-Free Monoids: $a^n = b^n \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ in a multiplicatively torsion-free monoid $M$ and any nonzero natural number $n$, the equality $a^n = b^n$ holds if and only if $a = b$.
zpow_left_injective theorem
: ∀ {n : ℤ}, n ≠ 0 → Injective fun a : G ↦ a ^ n
Full source 
@[to_additive zsmul_right_injective]
lemma zpow_left_injective : ∀ {n : ℤ}, n ≠ 0 → Injective fun a : G ↦ a ^ n
  | (n + 1 : ℕ), _ => by
    simpa [← Int.natCast_one, ← Int.natCast_add] using pow_left_injective n.succ_ne_zero
  | .negSucc n, _ => by simpa using inv_injective.comp (pow_left_injective n.succ_ne_zero)
Injectivity of the $n$-th power map in torsion-free groups
Informal description
For any group $G$ and any nonzero integer $n$, the $n$-th power function $a \mapsto a^n$ is injective on $G$.
zpow_left_inj theorem
(hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b
Full source 
@[to_additive zsmul_right_inj]
lemma zpow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (zpow_left_injective hn).eq_iff
Power Equality Criterion in Torsion-Free Groups: $a^n = b^n \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ in a torsion-free group $G$ and any nonzero integer $n$, the equality $a^n = b^n$ holds if and only if $a = b$.
zpow_eq_zpow_iff' theorem
(hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b
Full source 
/-- Alias of `zpow_left_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
`zsmul_lt_zsmul_iff'`. -/
@[to_additive "Alias of `zsmul_right_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
`zsmul_lt_zsmul_iff'`."]
lemma zpow_eq_zpow_iff' (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := zpow_left_inj hn
Power Equality Criterion in Torsion-Free Groups: $a^n = b^n \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ in a torsion-free group $G$ and any nonzero integer $n$, the equality $a^n = b^n$ holds if and only if $a = b$.