mathlib3

11439d8c - chore(algebra/direct_sum/internal): add missing simp lemmas (#10154)

chore(algebra/direct_sum/internal): add missing simp lemmas (#10154) These previously weren't needed when these were `@[reducible] def`s as `simp` saw right through them.