Def CompleteOrthogonalIdempotents.ringEquivOfComm

Modification history

2025-04-14 11:42
Mathlib/RingTheory/Idempotents.lean
chore(RingTheory/Idempotents): fix names (#24030)
Added CompleteOrthogonalIdempotents.ringEquivOfCommView on Github →