Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-06 20:28 38422449

View on Github →

fix(linear_algebra/subtype): simplify lifted operations by using projections instead of match

Estimated changes

modified theorem add_val
modified theorem neg_val
modified theorem smul_val