Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.fin_two_prod_one

Modification history

2022-07-11 14:26

src/linear_algebra/basis.lean

feat(linear_algebra): basis on R × R, and relation between matrices and linear maps in this basis (#15119)

Added basis.fin_two_prod_one View on Github →