mathlib3

03a6c95d - chore(ring_theory/ideal): use `ideal.mul_mem_left` instead of `ideal.smul_mem` (#6704)

chore(ring_theory/ideal): use `ideal.mul_mem_left` instead of `ideal.smul_mem` (#6704) Lots of proofs are relying on the fact that mul and smul are defeq, but this makes them hard to follow, as the goal state never contains the smul referenced by these lemmas.