mathlib3

a783a47c - feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303)

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