Commit 2021-10-25 20:31 e808b419
View on Github →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.