Commit 2026-06-19 19:54 5392b8aa

View on Github →

chore: move RingQuot results (#40823) This is prework for swapping FreeProduct to use RingCon instead of RingQuot; at which point this would allow the import to be removed from that file entirely. I renamed R to S in the move, to match the ambient variables in the destination. I haven't attempted to golf the proofs since my intent is to ultimately deprecate the entire destination file.

Estimated changes