feat(data/matrix): little lemmas on `map` (#4874)
I had a couple of expressions involving mapping matrices, that the simplifier didn't `simp` away. It turns out the missing lemmas already existed, just not with the correct form / hypotheses. So here they are.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
