Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.coe_smul_right

Modification history

2021-09-24 06:10

src/linear_algebra/basic.lean

feat(linear_algebra): redefine `linear_map` and `linear_equiv` to be semilinear (#9272) …

Modified linear_map.coe_smul_right View on Github →

2021-04-11 01:51

src/linear_algebra/basic.lean

feat(analysis/normed_space/finite_dimension): set of `f : E →L[𝕜] F` of rank `≥n` is open (#7022)

Added linear_map.coe_smul_right View on Github →