mathlib

b88d81c8 - feat(ring_theory/ideal/quotient_operations): add double quotient of an algebra (#18452)

feat(ring_theory/ideal/quotient_operations): add double quotient of an algebra (#18452) This adds definitions and lemmas on the double quotient `A / (I ⊔ J)` of a commutative algebra `A` by ideals `I` and `J`, analogous to existing definitions and lemmas on the double quotient of a commutative ring. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>