mathlib3

1f370bb4 - feat(linear_algebra/pi): linear_map.vec_cons and friends (#11343)

feat(linear_algebra/pi): linear_map.vec_cons and friends (#11343) The idea of these definitions is to be able to define a map as `x ↦ ![f₁ x, f₂ x, f₃ x]`, where `f₁ f₂ f₃` are already linear maps, as `f₁.vec_cons $ f₂.vec_cons $ f₃.vec_cons $ vec_empty`. This adds the same thing for bilinear maps as `x y ↦ ![f₁ x y, f₂ x y, f₃ x y]`. While the same thing could be achieved using `linear_map.pi ![f₁, f₂, f₃]`, this is not definitionally equal to the result using `linear_map.vec_cons`, as `fin.cases` and function application do not commute definitionally. Versions for when `f₁ f₂ f₃` are bilinear maps are also provided.