mathlib3

5a9ca8d3 - feat(linear_algebra/sesquilinear_form): add composition between sesquilinear forms and linear maps (#5729)

feat(linear_algebra/sesquilinear_form): add composition between sesquilinear forms and linear maps (#5729) Add composition lemmas for sesquilinear forms, that is, given a sesquilinear form and linear maps, a new sesquilinear form is induced by applying the arguments with the linear map.