Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.lsmul_injective

Modification history

2021-03-09 21:43
src/algebra/algebra/tower.lean
feat(algebra,linear_algebra): `{smul,lmul,lsmul}_injective` (#6588) …
Added algebra.lsmul_injectiveView on Github →