Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-18 12:28 e3e0aa0d

View on Github →

chore(linear_algebra/direct_sum_module): add dosctrings (#3418)

Estimated changes

modified def direct_sum.lmk