Commit 2021-03-09 21:43 5d82d1d4

View on Github →

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.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem algebra.lmul_injective

added theorem algebra.lmul_left_injective

added theorem algebra.lmul_right_injective

Modified src/algebra/algebra/tower.lean

added theorem algebra.lsmul_injective

Modified src/algebra/group_with_zero/defs.lean

added theorem mul_left_injective'

added theorem mul_right_injective'

Modified src/algebra/module/basic.lean

added theorem smul_injective

Modified src/linear_algebra/tensor_product.lean

added theorem linear_map.lsmul_injective