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-10-31 17:41
src/linear_algebra/basic.lean
chore(group_theory/group_action): introduce `smul_comm_class` (#4770)
Added linear_map.applyₗ'View on Github →