Commit 2021-01-06 16:21 f4128dc4

chore(ring_theory/ideal/basic): Make an argument to mul_mem_{left,right} explicit (#5611) Before this change, the lemmas with result a * b ∈ I did not have enough explicit arguments to determine both a and b, such as I.mul_mem_left hb. This resulted in callers using show, @, or sometimes ignoring the API and using smul_mem which does have appropriate argument explicitness. These callers have been cleaned up accordingly.