Theorems · Definition · group theory
AddCommGroup.torsion
(G : Type u_1) → [inst : AddCommGroup G] → AddSubgroup G
The torsion additive subgroup of an additive abelian group.
- Defined in
- Mathlib.GroupTheory.Torsion
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 43 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- AddSubgroupstatement · cited by 3,232
- AddSubmonoidproof · cited by 1,178
- AddCommMonoid.addTorsionproof · cited by 12
Cited by19
Results whose statement or proof uses this declaration.
- AddCommGroup.freeRankproof · cited by 6
- AddCommGroup.le_comap_torsionstatement · cited by 2
- AddCommGroup.mem_torsionstatement · cited by 2
- AddEquiv.comap_torsionstatement · cited by 1
- AddCommGroup.finite_torsion_of_descentstatement · cited by 1
- AddEquiv.map_torsionstatement and proof · cited by 1
- finrank_quotient_torsion_eqstatement · cited by 1
- AddCommGroup.torsion_eq_top_iffstatement and proof · cited by 1
- AddCommGroup.torsion_eq_torsion_addSubmonoidstatement · cited by 1
- Submodule.torsion_intstatement · cited by 1
- AddCommGroup.comap_torsion_of_injectivestatement · cited by 1
- AddCommGroup.finite_torsion_of_descent'statement · cited by 0