Commit 2026-06-23 00:12 2c4e038a
View on Github →refactor: switch from RingQuot to RingCon.Quotient (#40451)
This PR observes that RingQuot r is analogous to (ringConGen r).Quotient, and changes all callers to use the latter.
Note that RingQuot had some extra irreducibility that has not yet been configured for RingCon.Quotient, and so there is a performance drop associated with the switch.
Zulip: #mathlib4 > Canonical way to quotient a ring @ 💬