Mathlib v3 is deprecated. Go to Mathlib v4

Def linear_map.applyₗ

Modification history

2021-02-09 00:54
src/linear_algebra/basic.lean
chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs (#5899)
Modified linear_map.applyₗView on Github →
2020-09-10 05:42
src/linear_algebra/basic.lean
feat(linear_algebra): tiny missing pieces (#4089) …
Added linear_map.applyₗView on Github →