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

Modified src/algebra/direct_sum.lean

modified def direct_sum.mk

modified def direct_sum.of

modified theorem direct_sum.to_group.unique

modified def direct_sum.to_group

Modified src/linear_algebra/direct_sum/tensor_product.lean

Modified src/linear_algebra/direct_sum_module.lean

modified theorem direct_sum.apply_eq_component

modified def direct_sum.component

modified theorem direct_sum.ext

modified theorem direct_sum.ext_iff

modified def direct_sum.lmk

modified def direct_sum.lof

modified theorem direct_sum.to_module.ext

modified theorem direct_sum.to_module.unique

modified def direct_sum.to_module