mathlib

e5820f6c - chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen (#17892)

chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen (#17892) It's not clear to me whether it's worth keeping `ring_quot.rel r` around, or if it would be better to replace it entirely with `ring_con_gen`.