Commit 2021-02-03 12:26 5a9ca8d3

View on Github →

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.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

modified theorem bilin_form.comp_injective

Modified src/linear_algebra/sesquilinear_form.lean

added def sesq_form.comp

added theorem sesq_form.comp_apply

added theorem sesq_form.comp_comp

added theorem sesq_form.comp_injective

added def sesq_form.comp_left

added theorem sesq_form.comp_left_apply

added theorem sesq_form.comp_left_comp_right

added def sesq_form.comp_right

added theorem sesq_form.comp_right_apply

added theorem sesq_form.comp_right_comp_left