Commit 2024-02-13 12:46 a8eca770

View on Github →

chore(FinsuppVectorSpace): golf, Fintype -> Finite (#10464)

Golf Finset.sum_single_ite. Should it go to another file?
Assume Finite instead of Fintype in equivFun_symm_stdBasis.

Estimated changes

Modified Mathlib/LinearAlgebra/FinsuppVectorSpace.lean

modified theorem Basis.equivFun_symm_stdBasis

modified theorem Finset.sum_single_ite