Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-11 18:49 0f085b98

View on Github →

chore(linear_algebra/finite_dimensional): rename of_finite_basis (#4562)

  • rename of_finite_basis to of_fintype_basis;
  • add new of_finite_basis assuming that the domain the basis is a finite set;
  • allow s : finset ι and any function s → V in of_finset_basis.

Estimated changes