Commit 2021-07-15 16:32 a783a47c
View on Github →feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303) This also moves some imports around to make the star operator on vectors available in matrix/basic.lean This is a follow up to #8291