Theorem LinearMap.ker_smul'

Modification history

2024-02-14 03:21

Mathlib/Algebra/Module/Submodule/Ker.lean

chore: Move LinearMap.ker to a new file (#10233) …

Modified LinearMap.ker_smul'View on Github →

2023-06-04 14:19

Mathlib/LinearAlgebra/Basic.lean

style: allow `_` for an argument in `notation3` & replace `_foo` with `_` in `notation3` (#4652)

Modified LinearMap.ker_smul'View on Github →

2023-04-28 21:59

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Matrix.Diagonal (#3695) …

Modified LinearMap.ker_smul'View on Github →

2023-02-13 06:07

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Basic (#1979)

Added LinearMap.ker_smul'View on Github →