mathlib3

b26e15a4 - refactor(ring_theory/ideal/quotient): extract a `ring_con` structure (#17833)

refactor(ring_theory/ideal/quotient): extract a `ring_con` structure (#17833) The intent here is to remove some duplication with `ring_quot`. I've only copied across the basic lemmas from `group_theory/congruence`; I imagine most of the rest won't be that useful, and that if we do want them, we should look for a means to deduplicate them. Note that `ring_con.quotient` can be used to take quotients of semirings.