mathlib

48e3d6a4 - feat(linear_algebra/linear_pmap): add_action and mul_action (#16068)

feat(linear_algebra/linear_pmap): add_action and mul_action (#16068) This PR defines the instances `has_vadd`, `add_action` and `mul_action` for `linear_pmap`. Co-authored-by: Moritz Doll <doll@uni-bremen.de> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>