Documentation Verification Report

NonZeroDivisors

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

Statistics

Metric	Count
Definitions	0
Theorems `nsmul_injective`, `nsmul_injective`, `isUnit_of_finite`, `pow_injective`, `pow_right_inj`, `pow_right_injective`, `pow_right_injective₀`, `pow_right_inj₀`, `isUnit_of_finite`, `pow_injective`, `dvd_cancel_left_coe_nonZeroDivisors`, `dvd_cancel_left_mem_nonZeroDivisors`, `dvd_cancel_right_coe_nonZeroDivisors`, `dvd_cancel_right_mem_nonZeroDivisors`, `isLeftRegular_iff_mem_nonZeroDivisorsLeft`, `isRegular_iff_isUnit_of_finite`, `isRegular_iff_mem_nonZeroDivisors`, `isRightRegular_iff_mem_nonZeroDivisorsRight`, `isUnit_iff_mem_nonZeroDivisors_of_finite`, `le_nonZeroDivisorsLeft_iff_isLeftRegular`, `le_nonZeroDivisorsRight_iff_isRightRegular`, `le_nonZeroDivisors_iff_isRegular`, `mul_cancel_left_coe_nonZeroDivisors`, `mul_cancel_left_mem_nonZeroDivisors`, `mul_cancel_left_mem_nonZeroDivisorsLeft`, `mul_cancel_right_coe_nonZeroDivisors`, `mul_cancel_right_mem_nonZeroDivisors`, `mul_cancel_right_mem_nonZeroDivisorsRight`	28
Total	28

IsAddLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmul_injective` 📖	mathematical	`IsAddLeftRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`nsmul_eq_zero_iff_left` `add_left_eq_self_iff` `nsmul` `add_nsmul`

IsAddRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nsmul_injective` 📖	mathematical	`IsAddRightRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`AddOpposite.unop_injective` `IsAddLeftRegular.nsmul_injective` `AddOpposite.instAddTorsionFree` `isAddLeftRegular_op` `Iff.not` `AddOpposite.op_eq_zero_iff`

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_of_finite` 📖	mathematical	`IsLeftRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsUnit`	—	`IsUnit.isUnit_iff_mulLeft_bijective` `Finite.injective_iff_bijective`
`pow_injective` 📖	mathematical	`IsLeftRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`pow_eq_one_iff_right` `mul_left_eq_self_iff` `pow` `pow_add`

IsMulTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_right_inj` 📖	mathematical	—	`Monoid.toNatPow` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid`	—	`pow_right_injective`
`pow_right_injective` 📖	mathematical	—	`Monoid.toNatPow` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid`	—	`IsLeftRegular.pow_injective` `IsLeftRegular.all` `LeftCancelSemigroup.toIsLeftCancelMul`
`pow_right_injective₀` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`IsLeftRegular.pow_injective` `IsLeftCancelMulZero.mul_left_cancel_of_ne_zero`
`pow_right_inj₀` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`pow_right_injective₀`

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_of_finite` 📖	mathematical	`IsRightRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsUnit`	—	`IsUnit.isUnit_iff_mulRight_bijective` `Finite.injective_iff_bijective`
`pow_injective` 📖	mathematical	`IsRightRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`MulOpposite.unop_injective` `IsLeftRegular.pow_injective` `AddOpposite.instMulTorsionFree` `isLeftRegular_op` `Iff.not` `MulOpposite.op_eq_one_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_cancel_left_coe_nonZeroDivisors` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`dvd_cancel_left_mem_nonZeroDivisors` `Subtype.prop`
`dvd_cancel_left_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`IsLeftRegular.dvd_cancel_left` `isLeftRegular_iff_mem_nonZeroDivisorsLeft`
`dvd_cancel_right_coe_nonZeroDivisors` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`dvd_cancel_right_mem_nonZeroDivisors` `Subtype.prop`
`dvd_cancel_right_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing`	—	`mul_comm` `dvd_cancel_left_mem_nonZeroDivisors`
`isLeftRegular_iff_mem_nonZeroDivisorsLeft` 📖	mathematical	—	`IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsLeft`	—	`isLeftRegular_iff_right_eq_zero_of_mul`
`isRegular_iff_isUnit_of_finite` 📖	mathematical	—	`IsRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsUnit`	—	`IsLeftRegular.isUnit_of_finite` `IsRegular.left` `IsUnit.isRegular`
`isRegular_iff_mem_nonZeroDivisors` 📖	mathematical	—	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`isRegular_iff_eq_zero_of_mul`
`isRightRegular_iff_mem_nonZeroDivisorsRight` 📖	mathematical	—	`IsRightRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsRight`	—	`isRightRegular_iff_left_eq_zero_of_mul`
`isUnit_iff_mem_nonZeroDivisors_of_finite` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`isRegular_iff_mem_nonZeroDivisors` `isRegular_iff_isUnit_of_finite`
`le_nonZeroDivisorsLeft_iff_isLeftRegular` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisorsLeft` `Semiring.toMonoidWithZero` `IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Submonoid.instSetLike`	—	`instIsConcreteLE`
`le_nonZeroDivisorsRight_iff_isRightRegular` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisorsRight` `Semiring.toMonoidWithZero` `IsRightRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Submonoid.instSetLike`	—	`instIsConcreteLE`
`le_nonZeroDivisors_iff_isRegular` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.instMembership` `Submonoid.instSetLike`	—	—
`mul_cancel_left_coe_nonZeroDivisors` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`mul_cancel_left_mem_nonZeroDivisors` `Subtype.prop`
`mul_cancel_left_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`mul_cancel_left_mem_nonZeroDivisorsLeft`
`mul_cancel_left_mem_nonZeroDivisorsLeft` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsLeft`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`isLeftRegular_iff_mem_nonZeroDivisorsLeft`
`mul_cancel_right_coe_nonZeroDivisors` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`mul_cancel_right_mem_nonZeroDivisors` `Subtype.prop`
`mul_cancel_right_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`mul_cancel_right_mem_nonZeroDivisorsRight`
`mul_cancel_right_mem_nonZeroDivisorsRight` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsRight`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`isRightRegular_iff_mem_nonZeroDivisorsRight`

---

← Back to Index