mathlib3

22dce611 - feat(linear_algebra/linear_pmap): introduce notation (#15751)

feat(linear_algebra/linear_pmap): introduce notation (#15751) We add the notation `E →ₗ.[R] F` for `linear_pmap R E F` inspired by the notation for `pfun` and `linear_map`. Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>