Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `isAddRegular_iff`, `isAddRightRegular_iff`, `isAddRegular`, `isRegular_iff`, `isRightRegular_iff`, `add`, `add_left_eq_self_iff`, `nsmul`, `nsmul_iff`, `of_add`, `right_of_addCommute`, `add`, `and_of_add_of_add`, `nsmul`, `nsmul_iff`, `add`, `add_right_eq_self_iff`, `left_of_addCommute`, `nsmul`, `nsmul_iff`, `of_add`, `isAddRegular`, `iff_isAddLeftRegular_of_add_eq_zero`, `iff_isAddRightRegular_of_add_eq_zero`, `iff_isLeftRegular_of_mul_eq_one`, `iff_isRightRegular_of_mul_eq_one`, `mul`, `mul_left_eq_self_iff`, `of_mul`, `pow`, `pow_iff`, `right_of_commute`, `and_of_mul_of_mul`, `mul`, `pow`, `pow_iff`, `left_of_commute`, `mul`, `mul_right_eq_self_iff`, `of_mul`, `pow`, `pow_iff`, `isRegular`, `isRegular`, `add_isAddLeftRegular_iff`, `add_isAddRightRegular_iff`, `isAddLeftRegular_of_add_eq_zero`, `isAddRegular_add_and_add_iff`, `isAddRegular_add_iff`, `isAddRegular_zero`, `isAddRightRegular_of_add_eq_zero`, `isLeftRegular_of_mul_eq_one`, `isRegular_mul_and_mul_iff`, `isRegular_mul_iff`, `isRegular_one`, `isRightRegular_of_mul_eq_one`, `mul_isLeftRegular_iff`, `mul_isRightRegular_iff`	58
Total	58

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddRegular_iff` 📖	mathematical	`AddCommute`	`IsAddRegular` `IsAddLeftRegular`	—	`IsAddRegular.left` `IsAddLeftRegular.right_of_addCommute`
`isAddRightRegular_iff` 📖	mathematical	`AddCommute`	`IsAddRightRegular` `IsAddLeftRegular`	—	`IsAddRightRegular.left_of_addCommute` `IsAddLeftRegular.right_of_addCommute`

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddRegular` 📖	mathematical	—	`IsAddRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `val`	—	`isAddLeftRegular_of_add_eq_zero` `neg_add` `isAddRightRegular_of_add_eq_zero` `add_neg`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_iff` 📖	mathematical	`Commute`	`IsRegular` `IsLeftRegular`	—	`IsRegular.left` `IsLeftRegular.right_of_commute`
`isRightRegular_iff` 📖	mathematical	`Commute`	`IsRightRegular` `IsLeftRegular`	—	`IsRightRegular.left_of_commute` `IsLeftRegular.right_of_commute`

IsAddLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`IsAddLeftRegular` `AddSemigroup.toAdd`	—	—	`comp_add_left`
`add_left_eq_self_iff` 📖	mathematical	`IsAddLeftRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toZero`	—	`add_zero`
`nsmul` 📖	mathematical	`IsAddLeftRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`add_left_iterate` `Function.Injective.iterate`
`nsmul_iff` 📖	mathematical	—	`IsAddLeftRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`succ_nsmul` `of_add` `nsmul`
`of_add` 📖	—	`IsAddLeftRegular` `AddSemigroup.toAdd`	—	—	`Function.Injective.of_comp` `comp_add_left`
`right_of_addCommute` 📖	mathematical	`AddCommute` `IsAddLeftRegular`	`IsAddRightRegular`	—	`AddCommute.symm`

IsAddRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`IsAddRegular` `AddSemigroup.toAdd`	—	—	`IsAddLeftRegular.add` `left` `IsAddRightRegular.add` `right`
`and_of_add_of_add` 📖	—	`IsAddRegular` `AddSemigroup.toAdd`	—	—	`isAddRegular_add_and_add_iff`
`nsmul` 📖	mathematical	`IsAddRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`IsAddLeftRegular.nsmul` `left` `IsAddRightRegular.nsmul` `right`
`nsmul_iff` 📖	mathematical	—	`IsAddRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`IsAddLeftRegular.nsmul_iff` `left` `IsAddRightRegular.nsmul_iff` `right` `IsAddLeftRegular.nsmul` `IsAddRightRegular.nsmul`

IsAddRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`IsAddRightRegular` `AddSemigroup.toAdd`	—	—	`comp_add_right`
`add_right_eq_self_iff` 📖	mathematical	`IsAddRightRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toZero`	—	`zero_add`
`left_of_addCommute` 📖	mathematical	`AddCommute` `IsAddRightRegular`	`IsAddLeftRegular`	—	`AddCommute.symm_iff` `AddCommute.symm`
`nsmul` 📖	mathematical	`IsAddRightRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoid.toNatSMul`	—	`eq_1` `add_right_iterate` `Function.Injective.iterate`
`nsmul_iff` 📖	mathematical	—	`IsAddRightRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`succ_nsmul'` `of_add` `nsmul`
`of_add` 📖	—	`IsAddRightRegular` `AddSemigroup.toAdd`	—	—	`add_assoc`

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddRegular` 📖	mathematical	`IsAddUnit`	`IsAddRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`AddUnits.isAddRegular`

IsDedekindFiniteAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_isAddLeftRegular_of_add_eq_zero` 📖	mathematical	—	`IsDedekindFiniteAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `IsAddLeftRegular` `AddZero.toAdd`	—	`isAddLeftRegular_of_add_eq_zero` `add_eq_zero_symm` `add_assoc` `zero_add` `add_zero`
`iff_isAddRightRegular_of_add_eq_zero` 📖	mathematical	—	`IsDedekindFiniteAddMonoid` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `IsAddRightRegular` `AddZero.toAdd`	—	`isAddRightRegular_of_add_eq_zero` `add_eq_zero_symm` `add_assoc` `add_zero` `zero_add`

IsDedekindFiniteMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_isLeftRegular_of_mul_eq_one` 📖	mathematical	—	`IsDedekindFiniteMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsLeftRegular` `MulOne.toMul`	—	`isLeftRegular_of_mul_eq_one` `mul_eq_one_symm` `one_mul` `mul_one`
`iff_isRightRegular_of_mul_eq_one` 📖	mathematical	—	`IsDedekindFiniteMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsRightRegular` `MulOne.toMul`	—	`isRightRegular_of_mul_eq_one` `mul_eq_one_symm` `mul_assoc` `mul_one` `one_mul`

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul` 📖	—	`IsLeftRegular` `Semigroup.toMul`	—	—	`comp_mul_left`
`mul_left_eq_self_iff` 📖	mathematical	`IsLeftRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toOne`	—	`mul_one`
`of_mul` 📖	—	`IsLeftRegular` `Semigroup.toMul`	—	—	`Function.Injective.of_comp` `comp_mul_left`
`pow` 📖	mathematical	`IsLeftRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`Function.Injective.iterate`
`pow_iff` 📖	mathematical	—	`IsLeftRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`pow_succ` `of_mul` `pow`
`right_of_commute` 📖	mathematical	`Commute` `IsLeftRegular`	`IsRightRegular`	—	`Commute.symm`

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`and_of_mul_of_mul` 📖	—	`IsRegular` `Semigroup.toMul`	—	—	`isRegular_mul_and_mul_iff`
`mul` 📖	—	`IsRegular` `Semigroup.toMul`	—	—	`IsLeftRegular.mul` `left` `IsRightRegular.mul` `right`
`pow` 📖	mathematical	`IsRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`IsLeftRegular.pow` `left` `IsRightRegular.pow` `right`
`pow_iff` 📖	mathematical	—	`IsRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`IsLeftRegular.pow_iff` `left` `IsRightRegular.pow_iff` `right` `IsLeftRegular.pow` `IsRightRegular.pow`

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_of_commute` 📖	mathematical	`Commute` `IsRightRegular`	`IsLeftRegular`	—	`Commute.symm_iff` `Commute.symm`
`mul` 📖	—	`IsRightRegular` `Semigroup.toMul`	—	—	`comp_mul_right`
`mul_right_eq_self_iff` 📖	mathematical	`IsRightRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toOne`	—	`one_mul`
`of_mul` 📖	—	`IsRightRegular` `Semigroup.toMul`	—	—	`mul_assoc`
`pow` 📖	mathematical	`IsRightRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`eq_1` `mul_right_iterate` `Function.Injective.iterate`
`pow_iff` 📖	mathematical	—	`IsRightRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`pow_succ'` `of_mul` `pow`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular` 📖	mathematical	`IsUnit`	`IsRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`Units.isRegular`

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular` 📖	mathematical	—	`IsRegular` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `val`	—	`isLeftRegular_of_mul_eq_one` `inv_mul` `isRightRegular_of_mul_eq_one` `mul_inv`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_isAddLeftRegular_iff` 📖	—	`IsAddLeftRegular` `AddSemigroup.toAdd`	—	—	`IsAddLeftRegular.of_add` `IsAddLeftRegular.add`
`add_isAddRightRegular_iff` 📖	—	`IsAddRightRegular` `AddSemigroup.toAdd`	—	—	`IsAddRightRegular.of_add` `IsAddRightRegular.add`
`isAddLeftRegular_of_add_eq_zero` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	`IsAddLeftRegular`	—	`IsAddLeftRegular.of_add` `IsAddRegular.left` `isAddRegular_zero`
`isAddRegular_add_and_add_iff` 📖	mathematical	—	`IsAddRegular` `AddSemigroup.toAdd`	—	`IsAddLeftRegular.of_add` `IsAddRegular.left` `IsAddRightRegular.of_add` `IsAddRegular.right` `IsAddRegular.add`
`isAddRegular_add_iff` 📖	mathematical	—	`IsAddRegular` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`add_comm` `isAddRegular_add_and_add_iff`
`isAddRegular_zero` 📖	mathematical	—	`IsAddRegular` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`zero_add` `add_zero`
`isAddRightRegular_of_add_eq_zero` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	`IsAddRightRegular`	—	`IsAddRightRegular.of_add` `IsAddRegular.right` `isAddRegular_zero`
`isLeftRegular_of_mul_eq_one` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`IsLeftRegular`	—	`IsLeftRegular.of_mul` `IsRegular.left` `isRegular_one`
`isRegular_mul_and_mul_iff` 📖	mathematical	—	`IsRegular` `Semigroup.toMul`	—	`IsLeftRegular.of_mul` `IsRegular.left` `IsRightRegular.of_mul` `IsRegular.right` `IsRegular.mul`
`isRegular_mul_iff` 📖	mathematical	—	`IsRegular` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	`mul_comm` `isRegular_mul_and_mul_iff`
`isRegular_one` 📖	mathematical	—	`IsRegular` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`one_mul` `mul_one`
`isRightRegular_of_mul_eq_one` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`IsRightRegular`	—	`IsRightRegular.of_mul` `IsRegular.right` `isRegular_one`
`mul_isLeftRegular_iff` 📖	—	`IsLeftRegular` `Semigroup.toMul`	—	—	`IsLeftRegular.of_mul` `IsLeftRegular.mul`
`mul_isRightRegular_iff` 📖	—	`IsRightRegular` `Semigroup.toMul`	—	—	`IsRightRegular.of_mul` `IsRightRegular.mul`

---

← Back to Index