Commit 2025-10-15 10:28 4cea329f

View on Github →

chore(algebra): generalize mul_mem_smul_iff to rings (#30254) Generalize mul_mem_smul_iff to rings instead of just commutative rings.

Estimated changes

modified theorem Submodule.mul_mem_smul_iff