Theorem DirectSum.decompose_eq_mul_idempotent

Modification history

2025-01-20 12:14
Mathlib/Algebra/DirectSum/Idempotents.lean
feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition (#20531) …
Modified DirectSum.decompose_eq_mul_idempotentView on Github →
2025-01-04 18:55
Mathlib/Algebra/DirectSum/Idempotents.lean
feat(Algebra): more on `OrthogonalIdempotents` (#18195) …
Added DirectSum.decompose_eq_mul_idempotentView on Github →