Theorem LinearMap.lsmul_injective

Modification history

2026-01-13 19:40

Mathlib/LinearAlgebra/BilinearMap.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified LinearMap.lsmul_injective View on Github →

2023-02-28 06:48

Mathlib/LinearAlgebra/BilinearMap.lean

feat: port LinearAlgebra.BilinearMap (#2434)

Added LinearMap.lsmul_injective View on Github →