Commit 2025-04-14 11:42 9c2b8e16

View on Github →

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

Estimated changes

Modified Mathlib/RingTheory/Idempotents.lean

deleted def CompleteOrthogonalIdempotents.mulEquivOfComm

deleted def CompleteOrthogonalIdempotents.mulEquivOfIsMulCentral

added def CompleteOrthogonalIdempotents.ringEquivOfComm

added def CompleteOrthogonalIdempotents.ringEquivOfIsMulCentral