Commit 2021-10-23 17:11 0411b1e3
View on Github →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.