Torsion

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

Statistics

Metric	Count
Definitions	0
Theorems instIsAddTorsionFreeOfCharZero, map_neg, map_neg_one, map_sub_swap	4
Total	4

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAddTorsionFreeOfCharZero 📖	mathematical	—	IsAddTorsionFree AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	nsmul_eq_mul IsCancelMulZero.toIsLeftCancelMulZero toIsCancelMulZero

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_neg 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Monoid.toMulOneClass instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	neg_one_mul map_mul MonoidHomClass.toMulHomClass instMonoidHomClass map_neg_one one_mul
map_neg_one 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Monoid.toMulOneClass instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulOne.toOne	—	pow_eq_one_iff_left map_pow instMonoidHomClass neg_one_sq map_one MonoidHomClass.toOneHomClass
map_sub_swap 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring Monoid.toMulOneClass instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	map_neg neg_sub

---

← Back to Index