Commit 2023-04-07 10:44 d2c4d0ce

View on Github →

feat: port LinearAlgebra.FinsuppVectorSpace (#3294)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FinsuppVectorSpace.lean

added theorem Basis.equivFun_symm_stdBasis

added theorem Finset.sum_single_ite

added theorem Finset.sum_univ_ite

added theorem Finsupp.basis_repr

added theorem Finsupp.coe_basis

added theorem Finsupp.coe_basisSingleOne

added theorem Finsupp.linearIndependent_single