Torsion groups #

This file defines torsion groups, i.e. groups where all elements have finite order.

Main definitions #

Monoid.IsTorsion a predicate asserting G is torsion, i.e. that all elements are of finite order.
CommGroup.torsion G, the torsion subgroup of an abelian group G
CommMonoid.torsion G, the above stated for commutative monoids
Monoid.IsTorsionFree, asserting no nontrivial elements have finite order in G
AddMonoid.IsTorsion and AddMonoid.IsTorsionFree the additive versions of the above

Implementation #

All torsion monoids are really groups (which is proven here as Monoid.IsTorsion.group), but since the definition can be stated on monoids it is implemented on monoid to match other declarations in the group theory library.

Tags #

periodic group, aperiodic group, torsion subgroup, torsion abelian group

Future work #

generalize to π-torsion(-free) groups for a set of primes π
free, free solvable and free abelian groups are torsion free
complete direct and free products of torsion free groups are torsion free
groups which are residually finite p-groups with respect to 2 distinct primes are torsion free

source

def AddMonoid.IsTorsion (G : Type u_1) [AddMonoid G] :

Prop

A predicate on an additive monoid saying that all elements are of finite order.

Equations

AddMonoid.IsTorsion G = ∀ (g : G), IsOfFinAddOrder g

Instances For

source

def Monoid.IsTorsion (G : Type u_1) [Monoid G] :

Prop

A predicate on a monoid saying that all elements are of finite order.

Equations

Monoid.IsTorsion G = ∀ (g : G), IsOfFinOrder g

Instances For

source

@[simp]

theorem AddMonoid.not_isTorsion_iff (G : Type u_1) [AddMonoid G] :

¬AddMonoid.IsTorsion G ↔ ∃ (g : G), ¬IsOfFinAddOrder g

An additive monoid is not a torsion monoid if it has an element of infinite order.

source

@[simp]

theorem Monoid.not_isTorsion_iff (G : Type u_1) [Monoid G] :

¬Monoid.IsTorsion G ↔ ∃ (g : G), ¬IsOfFinOrder g

A monoid is not a torsion monoid if it has an element of infinite order.

source

theorem IsTorsion.addGroup.proof_2 {G : Type u_1} [AddMonoid G] :

∀ (a : G), zsmulRec 0 a = zsmulRec 0 a

source

noncomputable def IsTorsion.addGroup {G : Type u_1} [AddMonoid G] (tG : AddMonoid.IsTorsion G) :

AddGroup G

Torsion additive monoids are really additive groups

Equations

IsTorsion.addGroup tG = let src := inst; AddGroup.mk (_ : ∀ (g : G), -g + g = 0)

Instances For

source

theorem IsTorsion.addGroup.proof_5 {G : Type u_1} [AddMonoid G] (tG : AddMonoid.IsTorsion G) (g : G) :

-g + g = 0

source

theorem IsTorsion.addGroup.proof_4 {G : Type u_1} [AddMonoid G] :

∀ (n : ℕ) (a : G), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

source

theorem IsTorsion.addGroup.proof_1 {G : Type u_1} [AddMonoid G] :

∀ (a b : G), a - b = a - b

source

theorem IsTorsion.addGroup.proof_3 {G : Type u_1} [AddMonoid G] :

∀ (n : ℕ) (a : G), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

source

noncomputable def IsTorsion.group {G : Type u_1} [Monoid G] (tG : Monoid.IsTorsion G) :

Group G

Torsion monoids are really groups.

Equations

IsTorsion.group tG = let src := inst; Group.mk (_ : ∀ (g : G), g⁻¹ * g = 1)

Instances For

source

theorem IsTorsion.addSubgroup {G : Type u_1} [AddGroup G] (tG : AddMonoid.IsTorsion G) (H : AddSubgroup G) :

AddMonoid.IsTorsion ↥H

Subgroups of additive torsion groups are additive torsion groups.

source

theorem IsTorsion.subgroup {G : Type u_1} [Group G] (tG : Monoid.IsTorsion G) (H : Subgroup G) :

Monoid.IsTorsion ↥H

Subgroups of torsion groups are torsion groups.

source

theorem AddIsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (tG : AddMonoid.IsTorsion G) :

AddMonoid.IsTorsion H

The image of a surjective additive torsion group homomorphism is torsion.

source

theorem IsTorsion.of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (tG : Monoid.IsTorsion G) :

Monoid.IsTorsion H

The image of a surjective torsion group homomorphism is torsion.

source

theorem AddIsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hN : N = AddMonoidHom.ker f) (tH : AddMonoid.IsTorsion H) (tN : AddMonoid.IsTorsion ↥N) :

AddMonoid.IsTorsion G

Additive torsion groups are closed under extensions.

source

theorem IsTorsion.extension_closed {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hN : N = MonoidHom.ker f) (tH : Monoid.IsTorsion H) (tN : Monoid.IsTorsion ↥N) :

Monoid.IsTorsion G

Torsion groups are closed under extensions.

source

theorem AddIsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [AddGroup G] {N : AddSubgroup G} [AddGroup H] {f : G →+ H} (hf : Function.Surjective ⇑f) (hN : N = AddMonoidHom.ker f) (tN : AddMonoid.IsTorsion ↥N) :

AddMonoid.IsTorsion H ↔ AddMonoid.IsTorsion G

The image of a quotient is additively torsion iff the group is torsion.

source

theorem IsTorsion.quotient_iff {G : Type u_1} {H : Type u_2} [Group G] {N : Subgroup G} [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) (hN : N = MonoidHom.ker f) (tN : Monoid.IsTorsion ↥N) :

Monoid.IsTorsion H ↔ Monoid.IsTorsion G

The image of a quotient is torsion iff the group is torsion.

source

theorem ExponentExists.is_add_torsion {G : Type u_1} [AddGroup G] (h : AddMonoid.ExponentExists G) :

AddMonoid.IsTorsion G

If a group exponent exists, the group is additively torsion.

source

theorem ExponentExists.isTorsion {G : Type u_1} [Group G] (h : Monoid.ExponentExists G) :

Monoid.IsTorsion G

If a group exponent exists, the group is torsion.

source

theorem IsAddTorsion.exponentExists {G : Type u_1} [AddGroup G] (tG : AddMonoid.IsTorsion G) (bounded : Set.Finite (Set.range fun (g : G) => addOrderOf g)) :

AddMonoid.ExponentExists G

The group exponent exists for any bounded additive torsion group.

source

theorem IsTorsion.exponentExists {G : Type u_1} [Group G] (tG : Monoid.IsTorsion G) (bounded : Set.Finite (Set.range fun (g : G) => orderOf g)) :

Monoid.ExponentExists G

The group exponent exists for any bounded torsion group.

source

theorem is_add_torsion_of_finite {G : Type u_1} [AddGroup G] [Finite G] :

AddMonoid.IsTorsion G

Finite additive groups are additive torsion groups.

source

theorem isTorsion_of_finite {G : Type u_1} [Group G] [Finite G] :

Monoid.IsTorsion G

Finite groups are torsion groups.

source

theorem AddMonoid.IsTorsion.module_of_torsion (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Semiring R] [Module R M] (tR : AddMonoid.IsTorsion R) :

AddMonoid.IsTorsion M

A module whose scalars are additively torsion is additively torsion.

source

theorem AddMonoid.IsTorsion.module_of_finite (R : Type u_3) (M : Type u_4) [AddCommMonoid M] [Ring R] [Finite R] [Module R M] :

AddMonoid.IsTorsion M

A module with a finite ring of scalars is additively torsion.

source

theorem AddCommMonoid.addTorsion.proof_1 (G : Type u_1) [AddCommMonoid G] :

IsOfFinAddOrder 0

source

def AddCommMonoid.addTorsion (G : Type u_1) [AddCommMonoid G] :

AddSubmonoid G

The torsion submonoid of an additive commutative monoid.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CommMonoid.torsion (G : Type u_1) [CommMonoid G] :

Submonoid G

The torsion submonoid of a commutative monoid.

(Note that by Monoid.IsTorsion.group torsion monoids are truthfully groups.)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

abbrev AddCommMonoid.addTorsion.isTorsion.match_1 {G : Type u_1} [AddCommMonoid G] (motive : ↥(AddCommMonoid.addTorsion G) → Prop) :

∀ (x : ↥(AddCommMonoid.addTorsion G)), (∀ (x : G) (n : ℕ) (npos : n > 0) (hn : Function.IsPeriodicPt (fun (x_1 : G) => x + x_1) n 0), motive { val := x, property := (_ : ∃ n > 0, Function.IsPeriodicPt (fun (x_1 : G) => x + x_1) n 0) }) → motive x

Equations

(_ : motive x) = (_ : motive x)

Instances For

source

theorem AddCommMonoid.addTorsion.isTorsion {G : Type u_1} [AddCommMonoid G] :

AddMonoid.IsTorsion ↥(AddCommMonoid.addTorsion G)

Additive torsion submonoids are additively torsion.

source

theorem CommMonoid.torsion.isTorsion {G : Type u_1} [CommMonoid G] :

Monoid.IsTorsion ↥(CommMonoid.torsion G)

Torsion submonoids are torsion.

source

theorem AddCommMonoid.primaryComponent.proof_2 (G : Type u_1) [AddCommMonoid G] (p : ℕ) :

∃ (n : ℕ), addOrderOf 0 = p ^ n

source

theorem AddCommMonoid.primaryComponent.proof_1 (G : Type u_1) [AddCommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

∀ {a b : G}, a ∈ {g : G | ∃ (n : ℕ), addOrderOf g = p ^ n} → b ∈ {g : G | ∃ (n : ℕ), addOrderOf g = p ^ n} → ∃ (k : ℕ), addOrderOf (a + b) = p ^ k

source

def AddCommMonoid.primaryComponent (G : Type u_1) [AddCommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

AddSubmonoid G

The p-primary component is the submonoid of elements with additive order prime-power of p.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem AddCommMonoid.primaryComponent_coe (G : Type u_1) [AddCommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

↑(AddCommMonoid.primaryComponent G p) = {g : G | ∃ (n : ℕ), addOrderOf g = p ^ n}

source

@[simp]

theorem CommMonoid.primaryComponent_coe (G : Type u_1) [CommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

↑(CommMonoid.primaryComponent G p) = {g : G | ∃ (n : ℕ), orderOf g = p ^ n}

source

def CommMonoid.primaryComponent (G : Type u_1) [CommMonoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

Submonoid G

The p-primary component is the submonoid of elements with order prime-power of p.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem AddCommMonoid.primaryComponent.exists_orderOf_eq_prime_nsmul {G : Type u_1} [AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(AddCommMonoid.primaryComponent G p)) :

∃ (n : ℕ), addOrderOf g = p ^ n

Elements of the p-primary component have additive order p^n for some n

source

theorem CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow {G : Type u_1} [CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(CommMonoid.primaryComponent G p)) :

∃ (n : ℕ), orderOf g = p ^ n

Elements of the p-primary component have order p^n for some n.

source

theorem AddCommMonoid.primaryComponent.disjoint {G : Type u_1} [AddCommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')] (hne : p ≠ p') :

Disjoint (AddCommMonoid.primaryComponent G p) (AddCommMonoid.primaryComponent G p')

The p- and q-primary components are disjoint for p ≠ q.

source

theorem CommMonoid.primaryComponent.disjoint {G : Type u_1} [CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] {p' : ℕ} [hp' : Fact (Nat.Prime p')] (hne : p ≠ p') :

Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p')

The p- and q-primary components are disjoint for p ≠ q.

source

@[simp]

theorem AddMonoid.IsTorsion.torsion_eq_top {G : Type u_1} [AddCommMonoid G] (tG : AddMonoid.IsTorsion G) :

AddCommMonoid.addTorsion G = ⊤

The additive torsion submonoid of an additive torsion monoid is ⊤.

source

@[simp]

theorem Monoid.IsTorsion.torsion_eq_top {G : Type u_1} [CommMonoid G] (tG : Monoid.IsTorsion G) :

CommMonoid.torsion G = ⊤

The torsion submonoid of a torsion monoid is ⊤.

source

def AddMonoid.IsTorsion.torsionAddEquiv {G : Type u_1} [AddCommMonoid G] (tG : AddMonoid.IsTorsion G) :

↥(AddCommMonoid.addTorsion G) ≃+ G

An additive torsion monoid is isomorphic to its torsion submonoid.

Equations

AddMonoid.IsTorsion.torsionAddEquiv tG = AddEquiv.trans (AddEquiv.addSubmonoidCongr (_ : AddCommMonoid.addTorsion G = ⊤)) AddSubmonoid.topEquiv

Instances For

source

def Monoid.IsTorsion.torsionMulEquiv {G : Type u_1} [CommMonoid G] (tG : Monoid.IsTorsion G) :

↥(CommMonoid.torsion G) ≃* G

A torsion monoid is isomorphic to its torsion submonoid.

Equations

Monoid.IsTorsion.torsionMulEquiv tG = MulEquiv.trans (MulEquiv.submonoidCongr (_ : CommMonoid.torsion G = ⊤)) Submonoid.topEquiv

Instances For

source

theorem AddMonoid.IsTorsion.torsionAddEquiv_apply {G : Type u_1} [AddCommMonoid G] (tG : AddMonoid.IsTorsion G) (a : ↥(AddCommMonoid.addTorsion G)) :

(AddMonoid.IsTorsion.torsionAddEquiv tG) a = ↑((AddEquiv.addSubmonoidCongr (_ : AddCommMonoid.addTorsion G = ⊤)) a)

source

theorem Monoid.IsTorsion.torsionMulEquiv_apply {G : Type u_1} [CommMonoid G] (tG : Monoid.IsTorsion G) (a : ↥(CommMonoid.torsion G)) :

(Monoid.IsTorsion.torsionMulEquiv tG) a = ↑((MulEquiv.submonoidCongr (_ : CommMonoid.torsion G = ⊤)) a)

source

theorem AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe {G : Type u_1} [AddCommMonoid G] (tG : AddMonoid.IsTorsion G) (a : G) :

(AddEquiv.symm (AddMonoid.IsTorsion.torsionAddEquiv tG)) a = { val := ↑((AddEquiv.symm AddSubmonoid.topEquiv) a), property := (_ : IsOfFinAddOrder ↑((AddEquiv.symm AddSubmonoid.topEquiv) a)) }

source

theorem Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe {G : Type u_1} [CommMonoid G] (tG : Monoid.IsTorsion G) (a : G) :

(MulEquiv.symm (Monoid.IsTorsion.torsionMulEquiv tG)) a = { val := ↑((MulEquiv.symm Submonoid.topEquiv) a), property := (_ : IsOfFinOrder ↑((MulEquiv.symm Submonoid.topEquiv) a)) }

source

def AddCommMonoid.Torsion.ofTorsion (G : Type u_1) [AddCommMonoid G] :

↥(AddCommMonoid.addTorsion ↥(AddCommMonoid.addTorsion G)) ≃+ ↥(AddCommMonoid.addTorsion G)

Additive torsion submonoids of an additive torsion submonoid are isomorphic to the submonoid.

Equations

AddCommMonoid.Torsion.ofTorsion G = AddMonoid.IsTorsion.torsionAddEquiv (_ : AddMonoid.IsTorsion ↥(AddCommMonoid.addTorsion G))

Instances For

source

def Torsion.ofTorsion (G : Type u_1) [CommMonoid G] :

↥(CommMonoid.torsion ↥(CommMonoid.torsion G)) ≃* ↥(CommMonoid.torsion G)

Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.

Equations

Torsion.ofTorsion G = Monoid.IsTorsion.torsionMulEquiv (_ : Monoid.IsTorsion ↥(CommMonoid.torsion G))

Instances For

source

theorem AddCommGroup.torsion.proof_1 (G : Type u_1) [AddCommGroup G] :

∀ {x : G}, x ∈ (AddCommMonoid.addTorsion G).toAddSubsemigroup.carrier → IsOfFinAddOrder (-x)

source

def AddCommGroup.torsion (G : Type u_1) [AddCommGroup G] :

AddSubgroup G

The torsion subgroup of an additive abelian group.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CommGroup.torsion (G : Type u_1) [CommGroup G] :

Subgroup G

The torsion subgroup of an abelian group.

Equations

CommGroup.torsion G = let src := CommMonoid.torsion G; { toSubmonoid := src, inv_mem' := (_ : ∀ {x : G}, x ∈ (CommMonoid.torsion G).toSubsemigroup.carrier → IsOfFinOrder x⁻¹) }

Instances For

source

theorem AddCommGroup.add_torsion_eq_add_torsion_submonoid (G : Type u_1) [AddCommGroup G] :

AddCommMonoid.addTorsion G = (AddCommGroup.torsion G).toAddSubmonoid

The additive torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

source

theorem CommGroup.torsion_eq_torsion_submonoid (G : Type u_1) [CommGroup G] :

CommMonoid.torsion G = (CommGroup.torsion G).toSubmonoid

The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid.

source

theorem AddCommGroup.mem_torsion (G : Type u_1) [AddCommGroup G] (g : G) :

g ∈ AddCommGroup.torsion G ↔ IsOfFinAddOrder g

source

theorem CommGroup.mem_torsion (G : Type u_1) [CommGroup G] (g : G) :

g ∈ CommGroup.torsion G ↔ IsOfFinOrder g

source

abbrev AddCommGroup.primaryComponent.match_1 (G : Type u_1) [AddCommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] {g : G} :

let src := AddCommMonoid.primaryComponent G p; ∀ (motive : g ∈ src.carrier → Prop) (x : g ∈ src.carrier), (∀ (n : ℕ) (hn : addOrderOf g = p ^ n), motive (_ : ∃ (n : ℕ), addOrderOf g = p ^ n)) → motive x

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def AddCommGroup.primaryComponent (G : Type u_1) [AddCommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

AddSubgroup G

The p-primary component is the subgroup of elements with additive order prime-power of p.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem AddCommGroup.primaryComponent.proof_1 (G : Type u_1) [AddCommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] {g : G} :

g ∈ (AddCommMonoid.primaryComponent G p).toAddSubsemigroup.carrier → -g ∈ (AddCommMonoid.primaryComponent G p).toAddSubsemigroup.carrier

source

@[simp]

theorem CommGroup.primaryComponent_coe (G : Type u_1) [CommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

↑(CommGroup.primaryComponent G p) = {g : G | ∃ (n : ℕ), orderOf g = p ^ n}

source

@[simp]

theorem AddCommGroup.primaryComponent_coe (G : Type u_1) [AddCommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

↑(AddCommGroup.primaryComponent G p) = {g : G | ∃ (n : ℕ), addOrderOf g = p ^ n}

source

def CommGroup.primaryComponent (G : Type u_1) [CommGroup G] (p : ℕ) [hp : Fact (Nat.Prime p)] :

Subgroup G

The p-primary component is the subgroup of elements with order prime-power of p.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CommGroup.primaryComponent.isPGroup {G : Type u_1} [CommGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] :

IsPGroup p ↥(CommGroup.primaryComponent G p)

The p-primary component is a p group.

source

def AddMonoid.IsTorsionFree (G : Type u_1) [AddMonoid G] :

Prop

A predicate on an additive monoid saying that only 0 is of finite order.

Equations

AddMonoid.IsTorsionFree G = ∀ (g : G), g ≠ 0 → ¬IsOfFinAddOrder g

Instances For

source

def Monoid.IsTorsionFree (G : Type u_1) [Monoid G] :

Prop

A predicate on a monoid saying that only 1 is of finite order.

Equations

Monoid.IsTorsionFree G = ∀ (g : G), g ≠ 1 → ¬IsOfFinOrder g

Instances For

source

@[simp]

theorem AddMonoid.not_isTorsionFree_iff {G : Type u_1} [AddMonoid G] :

¬AddMonoid.IsTorsionFree G ↔ ∃ (g : G), g ≠ 0 ∧ IsOfFinAddOrder g

An additive monoid is not torsion free if any nontrivial element has finite order.

source

@[simp]

theorem Monoid.not_isTorsionFree_iff {G : Type u_1} [Monoid G] :

¬Monoid.IsTorsionFree G ↔ ∃ (g : G), g ≠ 1 ∧ IsOfFinOrder g

A nontrivial monoid is not torsion-free if any nontrivial element has finite order.

source

@[simp]

theorem AddMonoid.isTorsionFree_of_subsingleton {G : Type u_1} [AddMonoid G] [Subsingleton G] :

AddMonoid.IsTorsionFree G

source

@[simp]

theorem Monoid.isTorsionFree_of_subsingleton {G : Type u_1} [Monoid G] [Subsingleton G] :

Monoid.IsTorsionFree G

source

theorem AddMonoid.isTorsionFree_iff_torsion_eq_bot {G : Type u_3} [AddCommGroup G] :

AddMonoid.IsTorsionFree G ↔ AddCommGroup.torsion G = ⊥

source

theorem Monoid.isTorsionFree_iff_torsion_eq_bot {G : Type u_3} [CommGroup G] :

Monoid.IsTorsionFree G ↔ CommGroup.torsion G = ⊥

source

theorem AddMonoid.IsTorsion.not_torsion_free {G : Type u_1} [AddGroup G] [hN : Nontrivial G] :

AddMonoid.IsTorsion G → ¬AddMonoid.IsTorsionFree G

A nontrivial additive torsion group is not torsion-free.

source

theorem IsTorsion.not_torsion_free {G : Type u_1} [Group G] [hN : Nontrivial G] :

Monoid.IsTorsion G → ¬Monoid.IsTorsionFree G

A nontrivial torsion group is not torsion-free.

source

theorem AddMonoid.IsTorsionFree.not_torsion {G : Type u_1} [AddGroup G] [hN : Nontrivial G] :

AddMonoid.IsTorsionFree G → ¬AddMonoid.IsTorsion G

A nontrivial torsion-free additive group is not torsion.

source

theorem IsTorsionFree.not_torsion {G : Type u_1} [Group G] [hN : Nontrivial G] :

Monoid.IsTorsionFree G → ¬Monoid.IsTorsion G

A nontrivial torsion-free group is not torsion.

source

theorem IsTorsionFree.addSubgroup {G : Type u_1} [AddGroup G] (tG : AddMonoid.IsTorsionFree G) (H : AddSubgroup G) :

AddMonoid.IsTorsionFree ↥H

Subgroups of additive torsion-free groups are additively torsion-free.

source

theorem IsTorsionFree.subgroup {G : Type u_1} [Group G] (tG : Monoid.IsTorsionFree G) (H : Subgroup G) :

Monoid.IsTorsionFree ↥H

Subgroups of torsion-free groups are torsion-free.

source

theorem AddMonoid.IsTorsionFree.prod {η : Type u_3} {Gs : η → Type u_4} [(i : η) → AddGroup (Gs i)] (tfGs : ∀ (i : η), AddMonoid.IsTorsionFree (Gs i)) :

AddMonoid.IsTorsionFree ((i : η) → Gs i)

Direct products of additive torsion free groups are torsion free.

source

theorem IsTorsionFree.prod {η : Type u_3} {Gs : η → Type u_4} [(i : η) → Group (Gs i)] (tfGs : ∀ (i : η), Monoid.IsTorsionFree (Gs i)) :

Monoid.IsTorsionFree ((i : η) → Gs i)

Direct products of torsion free groups are torsion free.

source

theorem AddIsTorsionFree.quotient_torsion (G : Type u_1) [AddCommGroup G] :

AddMonoid.IsTorsionFree (G ⧸ AddCommGroup.torsion G)

Quotienting a group by its additive torsion subgroup yields an additive torsion free group.

source

theorem IsTorsionFree.quotient_torsion (G : Type u_1) [CommGroup G] :

Monoid.IsTorsionFree (G ⧸ CommGroup.torsion G)

Quotienting a group by its torsion subgroup yields a torsion free group.

Documentation

Mathlib.GroupTheory.Torsion

Torsion groups #

Main definitions #

Implementation #

Tags #

Future work #