Def CompleteOrthogonalIdempotents.ringEquivOfIsMulCentral

Modification history

2025-04-14 11:42

Mathlib/RingTheory/Idempotents.lean

chore(RingTheory/Idempotents): fix names (#24030)

Added CompleteOrthogonalIdempotents.ringEquivOfIsMulCentral View on Github →