Commit 2021-03-27 03:05 cfd1a4cb

feat(linear_algebra/bilinear_form): generalize some constructions to the noncomm case (#6824) Introduce an operation flip on a bilinear form, which swaps the arguments. Generalize the construction bilin_form.to_lin (which currently exists for commutative rings) to a weaker construction bilin_form.to_lin' for arbitrary rings. Rename lemmas sesq_form.map_sum_right -> sesq_form.sum_right sesq_form.map_sum_left -> sesq_form.sum_left bilin_form.map_sum_right -> bilin_form.sum_right bilin_form.map_sum_left -> bilin_form.sum_left to_linear_map_apply (sic, no namespace) -> bilin_form.to_lin_apply