mathlib3

0411b1e3 - feat(ring_theory/ideal): `simp` lemmas for `ideal.quotient.mk` + `algebra_map` (#9829)

feat(ring_theory/ideal): `simp` lemmas for `ideal.quotient.mk` + `algebra_map` (#9829) Some `simp` lemmas I needed for combining `algebra_map` with `ideal.quotient.mk`. This also allowed me to golf two existing proofs.