Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-01 11:28 9af7e5b5

View on Github →

refactor(linear_algebra/basic): use smul_right (#1640)

  • refactor(linear_algebra/basic): use smul_right
  • Update src/linear_algebra/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net
  • Update src/linear_algebra/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net

Estimated changes