Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-20 00:52 c832472d

View on Github →

chore(linear_algebra/basis): missing namespace (#17622)

Estimated changes

Modified src/linear_algebra/basis.lean

added theorem basis.coord_equiv_fun_symm

deleted theorem coord_equiv_fun_symm