Commit 2026-08-10 13:55 4f8e21b9
View on Github →feat(LocalRing): trivial generalization of RingEquiv.isLocalRing to non-commutative semirings (#42429)
Currently RingEquiv.isLocalRing is stated only for the case when one of the rings is commutative, but generalizing it to non-commutative rings only involves generalizing type classes.