mathlib3
cd012fbe - chore(ring_theory/ideal): use `ideal.mul_mem_left` instead of `submodule.smul_mem` (#12830)

Commit

3 years ago

chore(ring_theory/ideal): use `ideal.mul_mem_left` instead of `submodule.smul_mem` (#12830) In one place this saves one rewrite.

Author

eric-wieser

Parents