mathlib3

cef5898c - chore(linear_algebra): generalize conversion between matrices and bilinear forms to semirings (#14263)

chore(linear_algebra): generalize conversion between matrices and bilinear forms to semirings (#14263) Only one lemma was moved (`dual_distrib_apply`), none were renamed, and no proofs were meaningfully changed. Section markers were shuffled around, and some variables exchanged for variables with weaker typeclass assumptions. A few other things have been generalized to semiring at the same time; `linear_map.trace` and `linear_map.smul_rightₗ`