Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 09:02 9a338853

View on Github →

chore(data/matrix): rows and columns the right way around (#1171)

  • chore(data/matrix): rows and columns the right way around
  • update matrix.lean

Estimated changes

modified def matrix.col
modified def matrix.minor
modified def matrix.row