Torsion

📁 Source: Mathlib/Algebra/Group/Torsion.lean

Statistics

Metric	Count
Definitions	0
Theorems nsmul_eq_zero_iff', zsmul_eq_zero_iff, zsmul_eq_zero_iff_left, zsmul_eq_zero_iff_right, pow_eq_one_iff', zpow_eq_one_iff, zpow_eq_one_iff_left, zpow_eq_one_iff_right, to_isAddTorsionFree, to_isMulTorsionFree, instNoNatZeroDivisorsOfIsAddTorsionFree, inv_eq_self, inv_ne_self, neg_eq_self, neg_ne_self, nsmul_eq_zero_iff, nsmul_eq_zero_iff_left, nsmul_eq_zero_iff_right, nsmul_right_inj, nsmul_right_injective, pow_eq_one_iff, pow_eq_one_iff_left, pow_eq_one_iff_right, pow_left_inj, pow_left_injective, self_eq_inv, self_eq_neg, self_ne_inv, self_ne_neg, sq_eq_one, two_nsmul_eq_zero, zpow_eq_zpow_iff', zpow_left_inj, zpow_left_injective, zsmul_eq_zsmul_iff', zsmul_right_inj, zsmul_right_injective	37
Total	37

IsAddTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nsmul_eq_zero_iff' 📖	mathematical	—	AddMonoid.toNatSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	nsmul_eq_zero_iff_left
zsmul_eq_zero_iff 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_or_ne zero_zsmul zsmul_eq_zero_iff_right
zsmul_eq_zero_iff_left 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zsmul_eq_zero_iff
zsmul_eq_zero_iff_right 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zsmul_zero

IsMulTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_eq_one_iff' 📖	mathematical	—	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	pow_eq_one_iff_right
zpow_eq_one_iff 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	eq_or_ne zpow_zero
zpow_eq_one_iff_left 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	one_zpow
zpow_eq_one_iff_right 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_isAddTorsionFree 📖	mathematical	—	IsAddTorsionFree	—	Function.injective_of_subsingleton
to_isMulTorsionFree 📖	mathematical	—	IsMulTorsionFree	—	Function.injective_of_subsingleton

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNoNatZeroDivisorsOfIsAddTorsionFree 📖	mathematical	—	AddCommMonoid.toGrindNatModule	—	IsAddTorsionFree.nsmul_right_injective
inv_eq_self 📖	mathematical	—	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne	—	self_eq_inv
inv_ne_self 📖	—	—	—	—	Iff.ne inv_eq_self
neg_eq_self 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toZero	—	self_eq_neg
neg_ne_self 📖	—	—	—	—	Iff.ne neg_eq_self
nsmul_eq_zero_iff 📖	mathematical	—	AddMonoid.toNatSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	eq_or_ne zero_nsmul nsmul_eq_zero_iff_right
nsmul_eq_zero_iff_left 📖	mathematical	—	AddMonoid.toNatSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	nsmul_eq_zero_iff
nsmul_eq_zero_iff_right 📖	mathematical	—	AddMonoid.toNatSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	nsmul_zero
nsmul_right_inj 📖	mathematical	—	AddMonoid.toNatSMul	—	nsmul_right_injective
nsmul_right_injective 📖	mathematical	—	AddMonoid.toNatSMul	—	IsAddTorsionFree.nsmul_right_injective
pow_eq_one_iff 📖	mathematical	—	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	eq_or_ne pow_zero
pow_eq_one_iff_left 📖	mathematical	—	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	one_pow
pow_eq_one_iff_right 📖	mathematical	—	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	—
pow_left_inj 📖	mathematical	—	Monoid.toNatPow	—	pow_left_injective
pow_left_injective 📖	mathematical	—	Monoid.toNatPow	—	IsMulTorsionFree.pow_left_injective
self_eq_inv 📖	mathematical	—	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne	—	sq_eq_one sq mul_eq_one_iff_eq_inv
self_eq_neg 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toZero	—	two_nsmul_eq_zero two_nsmul add_eq_zero_iff_eq_neg
self_ne_inv 📖	—	—	—	—	Iff.ne self_eq_inv
self_ne_neg 📖	—	—	—	—	Iff.ne self_eq_neg
sq_eq_one 📖	mathematical	—	Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	pow_eq_one_iff_left
two_nsmul_eq_zero 📖	mathematical	—	AddMonoid.toNatSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	nsmul_eq_zero_iff_right
zpow_eq_zpow_iff' 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid	—	—
zpow_left_inj 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid	—	zpow_left_injective
zpow_left_injective 📖	mathematical	—	DivInvMonoid.toZPow Group.toDivInvMonoid	—	zpow_natCast pow_left_injective zpow_negSucc inv_injective
zsmul_eq_zsmul_iff' 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	—
zsmul_right_inj 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	zsmul_right_injective
zsmul_right_injective 📖	mathematical	—	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	natCast_zsmul nsmul_right_injective negSucc_zsmul neg_injective

---

← Back to Index