mathlib3

2f39bcbc - chore(ring_theory/ideal/quotient): add missing smul compatibility instances (#18934)

chore(ring_theory/ideal/quotient): add missing smul compatibility instances (#18934) The low priority is needed to avoid a timeout in what will be `ring_theory/kaehler.lean`. These instances are more general cases of the instances implied by `algebra α c.quotient` and `algebra α (R ⧸ I)`, which work for cases like `α = units R`.