Documentation Verification Report

Idempotent

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

Statistics

Metric	Count
Definitions `instComplSubtype`	1
Theorems `add`, `add_iff`, `add_sub_mul`, `add_sub_mul_of_commute`, `coe_compl`, `commute_of_anticommute`, `compl_compl`, `mul_eq_zero_of_anticommute`, `mul_one_sub_self`, `of_mul_add`, `one_compl`, `one_sub`, `one_sub_iff`, `one_sub_mul_self`, `sub`, `sub_iff`, `zero_compl`, `isIdempotentElem_iff_mul_one_sub_self`, `isIdempotentElem_iff_one_sub_mul_self`	19
Total	20

IsIdempotentElem

Definitions

Name	Category	Theorems
`instComplSubtype` 📖	CompOp	4 math math: `coe_compl`, `one_compl`, `zero_compl`, `compl_compl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `eq` `add_add_add_comm` `add_assoc` `zero_add`
`add_iff` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`add_right_cancel_iff` `IsCancelAdd.toIsRightCancelAdd` `add_assoc` `add_left_cancel_iff` `IsCancelAdd.toIsLeftCancelAdd` `add_add_add_comm` `zero_add` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `eq` `add`
`add_sub_mul` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toAdd`	—	`add_sub_mul_of_commute` `Commute.all`
`add_sub_mul_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `IsIdempotentElem`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd`	—	`Commute.eq` `mul_sub` `mul_add` `Distrib.leftDistribClass` `sub_mul` `add_mul` `Distrib.rightDistribClass` `eq` `mul_assoc` `add_sub_cancel_right` `mul_self_mul` `add_sub_cancel_left`
`coe_compl` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Compl.compl` `instComplSubtype` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`commute_of_anticommute` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Commute`	—	`mul_eq_zero_of_anticommute` `Commute.eq_1` `SemiconjBy.eq_1` `zero_add`
`compl_compl` 📖	mathematical	—	`Compl.compl` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `instComplSubtype`	—	`sub_sub_cancel`
`mul_eq_zero_of_anticommute` 📖	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`nsmul_zero` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `eq` `mul_assoc` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `add_zero`
`mul_one_sub_self` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mul_sub` `mul_one` `eq` `sub_self`
`of_mul_add` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsIdempotentElem`	—	`mul_one` `mul_add` `Distrib.leftDistribClass` `add_zero` `one_mul` `add_mul` `Distrib.rightDistribClass` `zero_add`
`one_compl` 📖	mathematical	—	`Compl.compl` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `instComplSubtype` `instOneSubtype` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `instZeroSubtype` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_self`
`one_sub` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`eq_1` `mul_sub` `mul_one` `sub_mul` `one_mul` `eq` `sub_self` `sub_zero`
`one_sub_iff` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`one_sub` `sub_sub_cancel`
`one_sub_mul_self` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_mul` `one_mul` `eq` `sub_self`
`sub` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`sub_mul` `mul_sub` `eq` `sub_self` `sub_zero`
`sub_iff` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`add_iff` `AddCancelMonoid.toIsCancelAdd` `add_sub_cancel` `add_sub` `eq` `sub_mul` `mul_sub` `add_sub_cancel_left` `mul_assoc` `add_mul` `Distrib.rightDistribClass` `add_sub_cancel_right` `mul_add` `Distrib.leftDistribClass` `Commute.eq` `zero_add` `two_nsmul` `sub_add` `sub_sub` `sub_add_cancel_right` `sub_neg_eq_add` `sub`
`zero_compl` 📖	mathematical	—	`Compl.compl` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `instComplSubtype` `instZeroSubtype` `NonUnitalNonAssocSemiring.toMulZeroClass` `instOneSubtype` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring`	—	`sub_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIdempotentElem_iff_mul_one_sub_self` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mul_sub` `mul_one` `sub_eq_zero` `IsIdempotentElem.eq_1`
`isIdempotentElem_iff_one_sub_mul_self` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`sub_mul` `one_mul` `sub_eq_zero` `IsIdempotentElem.eq_1`

---

← Back to Index