mathlib

379dd7d5 - chore(algebra/ring_quot): Provide `sub` explicitly to `ring_quot` (#7112)

chore(algebra/ring_quot): Provide `sub` explicitly to `ring_quot` (#7112) This means that using `ring_quot.mk (A - B) = ring_quot.mk A - ring_quot.mk B` is true by definition, even if `A - B = A + -B` is not true by definition.