mathlib

bf821223 - feat(algebra/direct_sum/basic): some lemmas about `direct_sum.of` (#10003)

feat(algebra/direct_sum/basic): some lemmas about `direct_sum.of` (#10003) Some small lemmas about `direct_sum.of` that are handy. Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>