Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-23 23:18 bad4f978

View on Github →

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

Estimated changes