Commit 2022-05-24 15:53 73a61259

View on Github →

feat(linear_algebra/bilinear_form): generalize scalar instances, fix diamonds (#14358) This fixes the zsmul and nsmul diamonds, makes sub definitionally better, and makes the scalar instance apply more generally. This also adds linear_map.comp_bilin_form. These changes bring the API more in line with quadratic_form.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

modified theorem bilin_form.add_apply

added theorem bilin_form.coe_add

added def bilin_form.coe_fn_add_monoid_hom

added theorem bilin_form.coe_injective

added theorem bilin_form.coe_neg

added theorem bilin_form.coe_smul

added theorem bilin_form.coe_sub

added theorem bilin_form.coe_zero

modified theorem bilin_form.neg_apply

modified theorem bilin_form.smul_apply

added theorem bilin_form.sub_apply

modified theorem bilin_form.zero_apply

added def linear_map.comp_bilin_form