Documentation Verification Report

Idempotent

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

Statistics

Metric	Count
Definitions `isIdempotentElemMulZeroAddOne`, `instBooleanAlgebraSubtypeIsIdempotentElem`, `instBooleanAlgebraSubtypeProdAndEqHMulFstSndOfNatHAdd`, `instComplSubtypeProdAndEqHMulFstSndOfNatHAdd`, `instLatticeSubtypeIsIdempotentElem`, `instOrderBotSubtypeIsIdempotentElem`, `instOrderTopSubtypeIsIdempotentElem`, `instPartialOrderSubtypeProdAndEqHMulFstSndOfNatHAdd`, `instSemilatticeInfSubtypeIsIdempotentElem`, `instSemilatticeSupSubtypeProdAndEqHMulFstSndOfNatHAdd`	10
Theorems `eq_of_mul_eq_add_eq_one`, `mul_eq_zero_add_eq_one_ext_left`, `mul_eq_zero_add_eq_one_ext_right`	3
Total	13

OrderIso

Definitions

Name	Category	Theorems
`isIdempotentElemMulZeroAddOne` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`instBooleanAlgebraSubtypeIsIdempotentElem` 📖	CompOp	—
`instBooleanAlgebraSubtypeProdAndEqHMulFstSndOfNatHAdd` 📖	CompOp	—
`instComplSubtypeProdAndEqHMulFstSndOfNatHAdd` 📖	CompOp	—
`instLatticeSubtypeIsIdempotentElem` 📖	CompOp	—
`instOrderBotSubtypeIsIdempotentElem` 📖	CompOp	—
`instOrderTopSubtypeIsIdempotentElem` 📖	CompOp	—
`instPartialOrderSubtypeProdAndEqHMulFstSndOfNatHAdd` 📖	CompOp	—
`instSemilatticeInfSubtypeIsIdempotentElem` 📖	CompOp	10 math math: `PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot`, `PrimeSpectrum.isIdempotentElemEquivClopens_one_sub`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup`, `PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens`, `PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_top`, `PrimeSpectrum.isIdempotentElemEquivClopens_mul`, `PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl`
`instSemilatticeSupSubtypeProdAndEqHMulFstSndOfNatHAdd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_mul_eq_add_eq_one` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`one_mul` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `mul_one`
`mul_eq_zero_add_eq_one_ext_left` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`eq_of_mul_eq_add_eq_one` `mul_comm`
`mul_eq_zero_add_eq_one_ext_right` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`eq_of_mul_eq_add_eq_one` `mul_comm` `add_comm`

---

← Back to Index