Idempotents

📁 Source: Mathlib/Algebra/DirectSum/Idempotents.lean

Statistics

Metric	Count
Definitions idempotent	1
Theorems completeOrthogonalIdempotents_idempotent, decompose_eq_mul_idempotent, isIdempotentElem_idempotent	3
Total	4

DirectSum

Definitions

Name	Category	Theorems
idempotent 📖	CompOp	3 math math: decompose_eq_mul_idempotent, isIdempotentElem_idempotent, completeOrthogonalIdempotents_idempotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completeOrthogonalIdempotents_idempotent 📖	mathematical	—	CompleteOrthogonalIdempotents idempotent	—	Submodule.addSubmonoidClass isIdempotentElem_idempotent decompose_eq_mul_idempotent idempotent.eq_1 decompose_coe of_eq_of_ne Submodule.coe_zero Equiv.injective DFunLike.ext decompose_sum DFinsupp.finset_sum_apply Finset.sum_congr of_apply Finset.sum_dite_eq'
decompose_eq_mul_idempotent 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike Equiv DirectSum AddSubmonoidClass.toAddCommMonoid Submodule.addSubmonoidClass EquivLike.toFunLike Equiv.instEquivLike decompose Distrib.toMul NonUnitalNonAssocSemiring.toDistrib idempotent	—	Submodule.addSubmonoidClass smul_eq_mul idempotent.eq_1 IsScalarTower.left Submodule.coe_smul smul_apply decompose_smul mul_one
isIdempotentElem_idempotent 📖	mathematical	—	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring idempotent	—	Submodule.addSubmonoidClass IsIdempotentElem.eq_1 decompose_eq_mul_idempotent idempotent.eq_1 decompose_coe of_eq_same

---

← Back to Index