Defs

📁 Source: Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean

Statistics

Metric	Count
Definitions NoZeroSMulDivisors	1
Theorems noZeroSMulDivisors, to_noZeroSMulDivisors_int, to_noZeroSMulDivisors_nat, toNoZeroSMulDivisors, eq_zero_or_eq_zero_of_smul_eq_zero, instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors, noZeroSMulDivisors_iff, noZeroSMulDivisors_iff_right_eq_zero_of_smul	8
Total	9

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noZeroSMulDivisors 📖	mathematical	—	NoZeroSMulDivisors	—	NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero

IsAddTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_noZeroSMulDivisors_int 📖	mathematical	—	NoZeroSMulDivisors MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	Mathlib.Tactic.Contrapose.contrapose₁ smul_zero zsmul_right_injective
to_noZeroSMulDivisors_nat 📖	mathematical	—	NoZeroSMulDivisors MulZeroClass.toZero Nat.instMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoid.toNatSMul	—	Mathlib.Tactic.Contrapose.contrapose₁ nsmul_zero nsmul_right_injective

NoZeroDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNoZeroSMulDivisors 📖	mathematical	—	NoZeroSMulDivisors	—	eq_zero_or_eq_zero_of_mul_eq_zero

NoZeroSMulDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_or_eq_zero_of_smul_eq_zero 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
NoZeroSMulDivisors 📖	CompData	8 math math: noZeroSMulDivisors_iff_right_eq_zero_of_smul, NoZeroDivisors.toNoZeroSMulDivisors, Function.noZeroSMulDivisors, IsAddTorsionFree.to_noZeroSMulDivisors_nat, noZeroSMulDivisors_iff, IsAddTorsionFree.to_noZeroSMulDivisors_int, Function.Injective.noZeroSMulDivisors, GroupWithZero.toNoZeroSMulDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors 📖	mathematical	—	Module.IsTorsionFree AddCommGroup.toAddCommMonoid	—	IsRegular.ne_zero IsDomain.toNontrivial NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero smul_sub sub_eq_zero
noZeroSMulDivisors_iff 📖	mathematical	—	NoZeroSMulDivisors	—	—
noZeroSMulDivisors_iff_right_eq_zero_of_smul 📖	mathematical	—	NoZeroSMulDivisors	—	—

---

← Back to Index