Theorem LinearMap.ker_lsmul

Modification history

2026-01-13 19:40

Mathlib/LinearAlgebra/BilinearMap.lean

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

Modified LinearMap.ker_lsmul View on Github →

2023-02-28 06:48

Mathlib/LinearAlgebra/BilinearMap.lean

feat: port LinearAlgebra.BilinearMap (#2434)

Added LinearMap.ker_lsmul View on Github →