Theorem CompleteOrthogonalIdempotents.pair_iff'ₛ

Modification history

2025-01-20 12:14
Mathlib/RingTheory/Idempotents.lean
feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition (#20531) …
Added CompleteOrthogonalIdempotents.pair_iff'ₛView on Github →