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.