Commit 2020-10-11 18:49 0f085b98
View on Github →chore(linear_algebra/finite_dimensional): rename of_finite_basis
(#4562)
- rename
of_finite_basis
toof_fintype_basis
; - add new
of_finite_basis
assuming that the domain the basis is afinite
set; - allow
s : finset ι
and any functions → V
inof_finset_basis
.