Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.eta_fin_two

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.eta_fin_twoView on Github →