Commit 2025-01-04 18:55 b43248be

View on Github →

feat(Algebra): more on OrthogonalIdempotents (#18195) Co-authored-by : @jjaassoonn

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/Idempotents.lean

added theorem DirectSum.completeOrthogonalIdempotents_idempotent

added theorem DirectSum.decompose_eq_mul_idempotent

added def DirectSum.idempotent

added theorem DirectSum.isIdempotentElem_idempotent

Modified Mathlib/RingTheory/Idempotents.lean