Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-18 22:51 cf1f8bcb

View on Github →

feat(linear_algebra/basis): add lemmas (#17606) From flt-regular.

Estimated changes

added theorem basis.coord_repr_symm
added theorem basis.dvd_coord_smul
added theorem coord_equiv_fun_symm