mathlib3

bad4f978 - feat(algebra/direct_sum): Add ⨁ notation (#3473)

feat(algebra/direct_sum): Add ⨁ notation (#3473) This uses the unicode character "n-ary circled plus operator", which seems to be the usual symbol for this operation Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>