Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.coord_equiv_fun_symm

Modification history

2022-11-20 00:52
src/linear_algebra/basis.lean
chore(linear_algebra/basis): missing namespace (#17622)
Added basis.coord_equiv_fun_symmView on Github →