Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.eta_fin_three

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_three View on Github →