Regular

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

Statistics

Metric	Count
Definitions	0
Theorems iff_eq_of_mul_left_eq_one, iff_eq_of_mul_right_eq_one, of_ne_zero', toIsCancelMulZero, isLeftRegular_of_non_zero_divisor, isRegular_iff_ne_zero', isRegular_of_ne_zero', isRightRegular_of_non_zero_divisor	8
Total	8

IsDedekindFiniteMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_eq_of_mul_left_eq_one 📖	mathematical	—	IsDedekindFiniteMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring	—	isDedekindFiniteMonoid_iff one_mul mul_one mul_add Distrib.leftDistribClass mul_sub mul_assoc sub_self zero_add sub_eq_zero right_eq_add AddRightCancelSemigroup.toIsRightCancelAdd
iff_eq_of_mul_right_eq_one 📖	mathematical	—	IsDedekindFiniteMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring	—	isDedekindFiniteMonoid_iff mul_assoc mul_one one_mul add_mul Distrib.rightDistribClass sub_mul sub_self zero_add sub_eq_zero right_eq_add AddRightCancelSemigroup.toIsRightCancelAdd

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_ne_zero' 📖	mathematical	—	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	isLeftRegular_of_non_zero_divisor NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero isRightRegular_of_non_zero_divisor

NoZeroDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsCancelMulZero 📖	mathematical	—	IsCancelMulZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsRegular.left IsRegular.of_ne_zero' IsRegular.right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeftRegular_of_non_zero_divisor 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	IsLeftRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	sub_eq_zero mul_sub
isRegular_iff_ne_zero' 📖	mathematical	—	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	IsRegular.left not_isLeftRegular_zero IsRegular.of_ne_zero'
isRegular_of_ne_zero' 📖	mathematical	—	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	IsRegular.of_ne_zero'
isRightRegular_of_non_zero_divisor 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	IsRightRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	sub_eq_zero sub_mul

---

← Back to Index