mathlib

407f39b0 - chore(ring_theory/matrix_algebra): golf using `matrix.map` (#15040)

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.