Idempotent

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

Statistics

Metric	Count
Definitions instZeroSubtype	1
Theorems coe_zero, iff_eq_zero_or_one, zero	3
Total	4

IsIdempotentElem

Definitions

Name	Category	Theorems
instZeroSubtype 📖	CompOp	3 math math: one_compl, zero_compl, coe_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_zero 📖	mathematical	—	IsIdempotentElem MulZeroClass.toMul instZeroSubtype MulZeroClass.toZero	—	—
iff_eq_zero_or_one 📖	mathematical	—	IsIdempotentElem MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulZeroClass.toZero MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	mul_left_cancel₀ mul_one zero one
zero 📖	mathematical	—	IsIdempotentElem MulZeroClass.toMul MulZeroClass.toZero	—	MulZeroClass.mul_zero

---

← Back to Index