Commit 2022-07-04 17:12 407f39b0

chore(ring_theory/matrix_algebra): golf using matrix.map (#15040) This replaces terms of the form λ i j, a * algebra_map R A (m i j) with the defeq a • m.map (algebra_map R A), as then we get access to the API about map. This also leverages existing bundled maps to avoid reproving linearity in the auxiliary constructions, removing to_fun and to_fun_right_linear as we can construct to_fun_bilinear directly with ease.