mathlib3

cfd1a4cb - feat(linear_algebra/bilinear_form): generalize some constructions to the noncomm case (#6824)

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`