Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.cons_vec_mul_cons

Modification history

2022-07-17 21:26

src/data/matrix/notation.lean

chore(linear_algebra/matrix): Use the new matrix notation in most places (#15306)

Added matrix.cons_vec_mul_cons View on Github →