Commit 2020-07-21 01:05 6721ddfb

refactor(ring_theory): remove unbundled leftovers in ideal.quotient (#3467) This PR aims to smooth some corners in the ideal.quotient namespace left by the move to bundled ring_homs. The main irritation is the ambiguity between different ways to map x : R to the quotient ring: quot.mk, quotient.mk, quotient.mk', submodule.quotient.mk, ideal.quotient.mk and ideal.quotient.mk_hom, which caused a lot of duplication and more awkward proofs. The specific changes are:

• delete function ideal_quotient.mk
• rename ring hom ideal.quotient.mk_hom to ideal.quotient.mk
• make new ideal_quotient.mk the simp normal form
• delete obsolete mk_eq_mk_hom
• delete obsolete mk_... simp lemmas (use ring_hom.map_... instead)
• delete quotient.map_mk which was unused and had no lemmas (ideal.map quotient.mk is used elsewhere)