Commit 2021-05-14 01:13 239908ee

feat(ring_theory/ideal/operations): add apply_coe_mem_map (#7566) This is a continuation of #7459. In this PR:

• We modify ideal.mem_map_of_mem in order to be consistent with submonoid.mem_map_of_mem.
• We modify submonoid.apply_coe_mem_map (and friends) to have the submonoid as an explicit variable. This was the case before #7459 (but with a different, and not consistent, name). It seems to me that this version makes the code more readable.
• We add ideal.apply_coe_mem_map (similar to submonoid.apply_coe_mem_map). Note that mem_map_of_mem is used in other places, for example we have multiset.mem_map_of_mem, but since a multiset is not a type there is no apply_coe_mem_map to add there.