Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information
1 parent
e6fab1d
commit 1f370bb
Showing
1 changed file
with
89 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters