mathlib3

5d82d1d4 - feat(algebra,linear_algebra): `{smul,lmul,lsmul}_injective` (#6588)

feat(algebra,linear_algebra): `{smul,lmul,lsmul}_injective` (#6588) This PR proves a few injectivity results for (scalar) multiplication in the setting of modules and algebras over a ring. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>