Torsion

📁 Source: Mathlib/GroupTheory/Torsion.lean

Statistics

Metric	Count
Definitions primaryComponent, torsion, ofTorsion, addTorsion, primaryComponent, IsTorsion, torsionAddEquiv, primaryComponent, torsion, primaryComponent, torsion, addGroup, group, IsTorsion, torsionMulEquiv, ofTorsion, instModuleQuotientAddSubgroupTorsion	17
Theorems add_torsion_eq_add_torsion_submonoid, coe_primaryComponent, isAddTorsionFree_iff_torsion_eq_bot, mem_torsion, isTorsion, coe_primaryComponent, disjoint, exists_orderOf_eq_prime_nsmul, extension_closed, of_surjective, quotient_iff, module_of_finite, module_of_torsion, torsionAddEquiv_apply, torsionAddEquiv_symm_apply_coe, torsion_eq_top, not_isTorsion_iff, coe_primaryComponent, isMulTorsionFree_iff_torsion_eq_bot, mem_torsion, isPGroup, torsion_eq_torsion_submonoid, coe_primaryComponent, disjoint, exists_orderOf_eq_prime_pow, isTorsion, isTorsion, is_add_torsion, exponentExists, addSubgroup, exponentExists, extension_closed, of_surjective, quotient_iff, subgroup, torsionMulEquiv_apply, torsionMulEquiv_symm_apply_coe, torsion_eq_top, not_isTorsion_iff, instIsAddTorsionFree, instIsMulTorsionFree, isTorsion_of_finite, is_add_torsion_of_finite, neg_one_mem_torsion, not_isAddTorsionFree_of_isTorsion, not_isMulTorsionFree_of_isTorsion, not_isTorsion_of_isAddTorsionFree, not_isTorsion_of_isMulTorsionFree	48
Total	65

AddCommGroup

Definitions

Name	Category	Theorems
primaryComponent 📖	CompOp	1 math math: coe_primaryComponent
torsion 📖	CompOp	5 math math: Submodule.torsion_int, mem_torsion, isAddTorsionFree_iff_torsion_eq_bot, QuotientAddGroup.instIsAddTorsionFree, add_torsion_eq_add_torsion_submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_torsion_eq_add_torsion_submonoid 📖	mathematical	—	AddCommMonoid.addTorsion toAddCommMonoid AddSubgroup.toAddSubmonoid toAddGroup torsion	—	—
coe_primaryComponent 📖	mathematical	—	SetLike.coe AddSubgroup toAddGroup AddSubgroup.instSetLike primaryComponent setOf addOrderOf AddCommMonoid.toAddMonoid toAddCommMonoid Monoid.toNatPow Nat.instMonoid	—	—
isAddTorsionFree_iff_torsion_eq_bot 📖	mathematical	—	IsAddTorsionFree SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddGroup torsion Bot.bot AddSubgroup AddSubgroup.instBot	—	isAddTorsionFree_iff_not_isOfFinAddOrder eq_bot_iff SetLike.le_def instIsConcreteLE not_imp_not mem_torsion AddSubgroup.mem_bot
mem_torsion 📖	mathematical	—	AddSubgroup toAddGroup SetLike.instMembership AddSubgroup.instSetLike torsion IsOfFinAddOrder SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—

AddCommMonoid

Definitions

Name	Category	Theorems
addTorsion 📖	CompOp	5 math math: AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe, addTorsion.isTorsion, AddMonoid.IsTorsion.torsion_eq_top, AddMonoid.IsTorsion.torsionAddEquiv_apply, AddCommGroup.add_torsion_eq_add_torsion_submonoid
primaryComponent 📖	CompOp	3 math math: primaryComponent.disjoint, primaryComponent.exists_orderOf_eq_prime_nsmul, coe_primaryComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_primaryComponent 📖	mathematical	—	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass toAddMonoid AddSubmonoid.instSetLike primaryComponent setOf addOrderOf Monoid.toNatPow Nat.instMonoid	—	—

AddCommMonoid.Torsion

Definitions

Name	Category	Theorems
ofTorsion 📖	CompOp	—

AddCommMonoid.addTorsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTorsion 📖	mathematical	—	AddMonoid.IsTorsion AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddCommMonoid.addTorsion AddSubmonoid.toAddMonoid	—	add_left_iterate add_zero AddSubmonoid.instAddSubmonoidClass AddSubmonoidClass.coe_nsmul isPeriodicPt_add_iff_nsmul_eq_zero

AddCommMonoid.primaryComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint 📖	mathematical	—	Disjoint AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder AddSubmonoid.instCompleteLattice AddCommMonoid.primaryComponent	—	AddSubmonoid.disjoint_def AddMonoid.addOrderOf_eq_one_iff pow_zero eq_of_prime_pow_eq Nat.instIsCancelMulZero Unique.instSubsingleton Nat.Prime.prime Fact.out
exists_orderOf_eq_prime_nsmul 📖	mathematical	—	addOrderOf AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddCommMonoid.primaryComponent AddSubmonoid.toAddMonoid Monoid.toNatPow Nat.instMonoid	—	addOrderOf_addSubmonoid

AddIsTorsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extension_closed 📖	—	AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoid.IsTorsion AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup	—	—	IsOfFinAddOrder.exists_nsmul_eq_zero AddMonoidHom.mem_ker AddMonoidHom.map_nsmul CanLift.prf Subtype.canLift isOfFinAddOrder_iff_nsmul_eq_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_nsmul AddSubgroup.coe_nsmul AddSubgroup.coe_zero
of_surjective 📖	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike AddMonoid.IsTorsion	—	—	AddMonoidHom.isOfFinAddOrder
quotient_iff 📖	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike AddMonoidHom.ker AddMonoid.IsTorsion AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup	—	—	extension_closed of_surjective

AddMonoid

Definitions

Name	Category	Theorems
IsTorsion 📖	MathDef	8 math math: is_add_torsion_of_finite, not_isTorsion_iff, ExponentExists.is_add_torsion, AddCommMonoid.addTorsion.isTorsion, isTorsion_iff_isTorsion_int, not_isTorsion_of_isAddTorsionFree, isTorsion_iff_isTorsion_nat, IsTorsion.module_of_finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isTorsion_iff 📖	mathematical	—	IsTorsion IsOfFinAddOrder	—	IsTorsion.eq_1

AddMonoid.IsTorsion

Definitions

Name	Category	Theorems
torsionAddEquiv 📖	CompOp	2 math math: torsionAddEquiv_symm_apply_coe, torsionAddEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
module_of_finite 📖	mathematical	—	AddMonoid.IsTorsion AddCommMonoid.toAddMonoid	—	module_of_torsion is_add_torsion_of_finite
module_of_torsion 📖	mathematical	AddMonoid.IsTorsion AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	AddCommMonoid.toAddMonoid	—	isOfFinAddOrder_iff_nsmul_eq_zero IsOfFinAddOrder.exists_nsmul_eq_zero Nat.cast_smul_eq_nsmul zero_smul
torsionAddEquiv_apply 📖	mathematical	AddMonoid.IsTorsion AddCommMonoid.toAddMonoid	DFunLike.coe AddEquiv AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddCommMonoid.addTorsion AddSubmonoid.add AddZero.toAdd AddZeroClass.toAddZero EquivLike.toFunLike AddEquiv.instEquivLike torsionAddEquiv Top.top AddSubmonoid.instTop AddEquiv.addSubmonoidCongr torsion_eq_top	—	—
torsionAddEquiv_symm_apply_coe 📖	mathematical	AddMonoid.IsTorsion AddCommMonoid.toAddMonoid	DFunLike.coe AddEquiv AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddCommMonoid.addTorsion AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm torsionAddEquiv Top.top AddSubmonoid.instTop AddSubmonoid.topEquiv	—	—
torsion_eq_top 📖	mathematical	AddMonoid.IsTorsion AddCommMonoid.toAddMonoid	AddCommMonoid.addTorsion Top.top AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instTop	—	AddSubmonoid.ext

CommGroup

Definitions

Name	Category	Theorems
primaryComponent 📖	CompOp	2 math math: coe_primaryComponent, primaryComponent.isPGroup
torsion 📖	CompOp	4 math math: QuotientGroup.instIsMulTorsionFree, isMulTorsionFree_iff_torsion_eq_bot, torsion_eq_torsion_submonoid, mem_torsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_primaryComponent 📖	mathematical	—	SetLike.coe Subgroup toGroup Subgroup.instSetLike primaryComponent setOf orderOf CommMonoid.toMonoid toCommMonoid Monoid.toNatPow Nat.instMonoid	—	—
isMulTorsionFree_iff_torsion_eq_bot 📖	mathematical	—	IsMulTorsionFree DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup torsion Bot.bot Subgroup Subgroup.instBot	—	isMulTorsionFree_iff_not_isOfFinOrder eq_bot_iff SetLike.le_def instIsConcreteLE
mem_torsion 📖	mathematical	—	Subgroup toGroup SetLike.instMembership Subgroup.instSetLike torsion IsOfFinOrder DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
torsion_eq_torsion_submonoid 📖	mathematical	—	CommMonoid.torsion toCommMonoid Subgroup.toSubmonoid toGroup torsion	—	—

CommGroup.primaryComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPGroup 📖	mathematical	—	IsPGroup Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike CommGroup.primaryComponent Subgroup.toGroup	—	exists_orderOf_eq_prime_pow_iff CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow

CommMonoid

Definitions

Name	Category	Theorems
primaryComponent 📖	CompOp	3 math math: primaryComponent.disjoint, primaryComponent.exists_orderOf_eq_prime_pow, coe_primaryComponent
torsion 📖	CompOp	6 math math: Monoid.IsTorsion.torsionMulEquiv_apply, Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe, CommGroup.torsion_eq_torsion_submonoid, Monoid.IsTorsion.torsion_eq_top, neg_one_mem_torsion, torsion.isTorsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_primaryComponent 📖	mathematical	—	SetLike.coe Submonoid Monoid.toMulOneClass toMonoid Submonoid.instSetLike primaryComponent setOf orderOf Monoid.toNatPow Nat.instMonoid	—	—

CommMonoid.primaryComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint 📖	mathematical	—	Disjoint Submonoid Monoid.toMulOneClass CommMonoid.toMonoid Submonoid.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Submonoid.instCompleteLattice CommMonoid.primaryComponent	—	Submonoid.disjoint_def orderOf_eq_one_iff pow_zero eq_of_prime_pow_eq Nat.instIsCancelMulZero Unique.instSubsingleton Nat.Prime.prime Fact.out
exists_orderOf_eq_prime_pow 📖	mathematical	—	orderOf Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike CommMonoid.primaryComponent Submonoid.toMonoid Monoid.toNatPow Nat.instMonoid	—	orderOf_submonoid

CommMonoid.torsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTorsion 📖	mathematical	—	Monoid.IsTorsion Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike CommMonoid.torsion Submonoid.toMonoid	—	mul_left_iterate mul_one Submonoid.instSubmonoidClass SubmonoidClass.coe_pow isPeriodicPt_mul_iff_pow_eq_one

ExponentExists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTorsion 📖	mathematical	Monoid.ExponentExists DivInvMonoid.toMonoid Group.toDivInvMonoid	Monoid.IsTorsion	—	isOfFinOrder_iff_pow_eq_one
is_add_torsion 📖	mathematical	AddMonoid.ExponentExists SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddMonoid.IsTorsion	—	isOfFinAddOrder_iff_nsmul_eq_zero

IsAddTorsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exponentExists 📖	mathematical	AddMonoid.IsTorsion SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddMonoid.ExponentExists	—	AddMonoid.exponent_ne_zero AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finite IsOfFinAddOrder.addOrderOf_pos

IsTorsion

Definitions

Name	Category	Theorems
addGroup 📖	CompOp	—
group 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroup 📖	mathematical	AddMonoid.IsTorsion SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.toAddGroup	—	AddSubmonoid.isOfFinAddOrder_coe
exponentExists 📖	mathematical	Monoid.IsTorsion DivInvMonoid.toMonoid Group.toDivInvMonoid	Monoid.ExponentExists	—	Monoid.exponent_ne_zero Monoid.exponent_ne_zero_iff_range_orderOf_finite IsOfFinOrder.orderOf_pos
extension_closed 📖	—	MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.IsTorsion Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	—	—	IsOfFinOrder.exists_pow_eq_one MonoidHom.mem_ker MonoidHom.map_pow CanLift.prf Subtype.canLift isOfFinOrder_iff_pow_eq_one mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono pow_mul Subgroup.coe_pow Subgroup.coe_one
of_surjective 📖	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike Monoid.IsTorsion	—	—	MonoidHom.isOfFinOrder
quotient_iff 📖	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike MonoidHom.ker Monoid.IsTorsion Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	—	—	extension_closed of_surjective
subgroup 📖	mathematical	Monoid.IsTorsion DivInvMonoid.toMonoid Group.toDivInvMonoid	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	—	Submonoid.isOfFinOrder_coe

Monoid

Definitions

Name	Category	Theorems
IsTorsion 📖	MathDef	5 math math: isTorsion_of_finite, not_isTorsion_iff, not_isTorsion_of_isMulTorsionFree, ExponentExists.isTorsion, CommMonoid.torsion.isTorsion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isTorsion_iff 📖	mathematical	—	IsTorsion IsOfFinOrder	—	IsTorsion.eq_1

Monoid.IsTorsion

Definitions

Name	Category	Theorems
torsionMulEquiv 📖	CompOp	2 math math: torsionMulEquiv_apply, torsionMulEquiv_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
torsionMulEquiv_apply 📖	mathematical	Monoid.IsTorsion CommMonoid.toMonoid	DFunLike.coe MulEquiv Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike CommMonoid.torsion Submonoid.mul MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike MulEquiv.instEquivLike torsionMulEquiv Top.top Submonoid.instTop MulEquiv.submonoidCongr torsion_eq_top	—	—
torsionMulEquiv_symm_apply_coe 📖	mathematical	Monoid.IsTorsion CommMonoid.toMonoid	DFunLike.coe MulEquiv Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike CommMonoid.torsion MulOne.toMul MulOneClass.toMulOne Submonoid.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm torsionMulEquiv Top.top Submonoid.instTop Submonoid.topEquiv	—	—
torsion_eq_top 📖	mathematical	Monoid.IsTorsion CommMonoid.toMonoid	CommMonoid.torsion Top.top Submonoid Monoid.toMulOneClass Submonoid.instTop	—	Submonoid.ext

QuotientAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddTorsionFree 📖	mathematical	—	IsAddTorsionFree HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup instHasQuotientAddSubgroup AddCommGroup.torsion SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quotient.addGroup AddSubgroup.normal_of_comm	—	IsAddTorsionFree.of_not_isOfFinAddOrder IsOfFinAddOrder.exists_nsmul_eq_zero AddSubgroup.normal_of_comm eq_zero_iff isOfFinAddOrder_iff_nsmul_eq_zero mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_nsmul

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMulTorsionFree 📖	mathematical	—	IsMulTorsionFree HasQuotient.Quotient Subgroup CommGroup.toGroup instHasQuotientSubgroup CommGroup.torsion DivInvMonoid.toMonoid Group.toDivInvMonoid Quotient.group Subgroup.normal_of_comm	—	IsMulTorsionFree.of_not_isOfFinOrder IsOfFinOrder.exists_pow_eq_one Subgroup.normal_of_comm eq_one_iff isOfFinOrder_iff_pow_eq_one mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono pow_mul

Torsion

Definitions

Name	Category	Theorems
ofTorsion 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instModuleQuotientAddSubgroupTorsion 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTorsion_of_finite 📖	mathematical	—	Monoid.IsTorsion DivInvMonoid.toMonoid Group.toDivInvMonoid	—	ExponentExists.isTorsion Monoid.ExponentExists.of_finite
is_add_torsion_of_finite 📖	mathematical	—	AddMonoid.IsTorsion SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	ExponentExists.is_add_torsion AddMonoid.ExponentExists.of_finite
neg_one_mem_torsion 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike CommMonoid.torsion InvolutiveNeg.toNeg HasDistribNeg.toInvolutiveNeg MulOne.toMul MulOneClass.toMulOne MulOne.toOne	—	zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid isPeriodicPt_mul_iff_pow_eq_one Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow
not_isAddTorsionFree_of_isTorsion 📖	mathematical	AddMonoid.IsTorsion SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	IsAddTorsionFree	—	not_isAddTorsionFree_iff_isOfFinAddOrder exists_ne
not_isMulTorsionFree_of_isTorsion 📖	mathematical	Monoid.IsTorsion DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	IsMulTorsionFree	—	not_isMulTorsionFree_iff_isOfFinOrder exists_ne
not_isTorsion_of_isAddTorsionFree 📖	mathematical	—	AddMonoid.IsTorsion SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	not_isAddTorsionFree_of_isTorsion
not_isTorsion_of_isMulTorsionFree 📖	mathematical	—	Monoid.IsTorsion DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	not_isMulTorsionFree_of_isTorsion

---

← Back to Index