Torsion

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

Statistics

Metric	Count
Definitions	0
Theorems mk', instIsMulTorsionFree	2
Total	2

IsMulTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk' 📖	mathematical	—	IsMulTorsionFree MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	isReduced_of_noZeroDivisors

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMulTorsionFree 📖	mathematical	—	IsMulTorsionFree MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	IsMulTorsionFree.mk' IsRightCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsRightCancelMulZero toIsCancelMulZero Associated.normalizedFactors_eq Associated.of_eq associated_iff_normalizedFactors_eq_normalizedFactors Multiset.instIsAddTorsionFree normalizedFactors_pow IsLeftRegular.pow IsLeftCancelMulZero.mul_left_cancel_of_ne_zero IsCancelMulZero.toIsLeftCancelMulZero mul_one Units.val_one pow_eq_one_iff_left Units.val_eq_one Units.val_pow_eq_pow_val IsLeftRegular.mul_left_eq_self_iff mul_pow

---

← Back to Index