Commit 2020-11-12 00:24 49cf28fe
View on Github →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.