mathlib3

e808b419 - feat(data/matrix/basic): lemmas about transpose and conj_transpose on sums and products (#9880)

feat(data/matrix/basic): lemmas about transpose and conj_transpose on sums and products (#9880) This also generalizes some previous results from `star_ring` to `star_add_monoid` now that the latter exists. To help prove the non-commutative statements, this adds `monoid_hom.unop_map_list_prod` and similar. This could probably used for proving `star_list_prod` in future. Co-authored-by: Johan Commelin <johan@commelin.net>