Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-07 17:18 5e42425d

View on Github →

fix(algebra/module): fix type universes in is_linear_map.sum

Estimated changes

Modified algebra/module.lean

modified theorem is_linear_map.sum