Documentation Verification Report

Regular

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

Statistics

Metric	Count
Definitions	0
Theorems `mul_left_eq_zero_iff`, `ne_zero`, `subsingleton`, `ne_zero`, `of_ne_zero`, `subsingleton`, `mul_right_eq_zero_iff`, `ne_zero`, `subsingleton`, `isLeftRegular_zero_iff_subsingleton`, `isRegular_iff_ne_zero`, `isRegular_iff_subsingleton`, `isRegular_of_ne_zero`, `isRightRegular_zero_iff_subsingleton`, `not_isLeftRegular_zero`, `not_isLeftRegular_zero_iff`, `not_isRegular_zero`, `not_isRightRegular_zero`, `not_isRightRegular_zero_iff`	19
Total	19

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_left_eq_zero_iff` 📖	mathematical	`IsLeftRegular` `MulZeroClass.toMul`	`MulZeroClass.toZero`	—	`MulZeroClass.mul_zero`
`ne_zero` 📖	—	`IsLeftRegular` `MulZeroClass.toMul`	—	—	`exists_pair_ne` `MulZeroClass.zero_mul`
`subsingleton` 📖	—	`IsLeftRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	—	`MulZeroClass.zero_mul`

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne_zero` 📖	—	`IsRegular` `MulZeroClass.toMul`	—	—	`IsLeftRegular.ne_zero` `left`
`of_ne_zero` 📖	mathematical	—	`IsRegular` `MulZeroClass.toMul`	—	`mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `mul_right_cancel₀` `IsCancelMulZero.toIsRightCancelMulZero`
`subsingleton` 📖	—	`IsRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	—	`IsLeftRegular.subsingleton` `left`

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_right_eq_zero_iff` 📖	mathematical	`IsRightRegular` `MulZeroClass.toMul`	`MulZeroClass.toZero`	—	`MulZeroClass.zero_mul`
`ne_zero` 📖	—	`IsRightRegular` `MulZeroClass.toMul`	—	—	`exists_pair_ne` `MulZeroClass.mul_zero`
`subsingleton` 📖	—	`IsRightRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	—	`MulZeroClass.mul_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLeftRegular_zero_iff_subsingleton` 📖	mathematical	—	`IsLeftRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	`IsLeftRegular.subsingleton`
`isRegular_iff_ne_zero` 📖	mathematical	—	`IsRegular` `MulZeroClass.toMul`	—	`IsRegular.ne_zero` `IsRegular.of_ne_zero`
`isRegular_iff_subsingleton` 📖	mathematical	—	`IsRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	`IsLeftRegular.subsingleton` `IsRegular.left` `isLeftRegular_zero_iff_subsingleton` `isRightRegular_zero_iff_subsingleton`
`isRegular_of_ne_zero` 📖	mathematical	—	`IsRegular` `MulZeroClass.toMul`	—	`IsRegular.of_ne_zero`
`isRightRegular_zero_iff_subsingleton` 📖	mathematical	—	`IsRightRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	`IsRightRegular.subsingleton`
`not_isLeftRegular_zero` 📖	mathematical	—	`IsLeftRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	`not_isLeftRegular_zero_iff`
`not_isLeftRegular_zero_iff` 📖	mathematical	—	`IsLeftRegular` `MulZeroClass.toMul` `MulZeroClass.toZero` `Nontrivial`	—	`nontrivial_iff` `not_iff_comm` `isLeftRegular_zero_iff_subsingleton` `subsingleton_iff`
`not_isRegular_zero` 📖	mathematical	—	`IsRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	`IsRegular.ne_zero`
`not_isRightRegular_zero` 📖	mathematical	—	`IsRightRegular` `MulZeroClass.toMul` `MulZeroClass.toZero`	—	`not_isRightRegular_zero_iff`
`not_isRightRegular_zero_iff` 📖	mathematical	—	`IsRightRegular` `MulZeroClass.toMul` `MulZeroClass.toZero` `Nontrivial`	—	`nontrivial_iff` `not_iff_comm` `isRightRegular_zero_iff_subsingleton` `subsingleton_iff`

---

← Back to Index