Theorem Finsupp.coe_basisSingleOne

Modification history

2023-04-07 10:44
Mathlib/LinearAlgebra/FinsuppVectorSpace.lean
feat: port LinearAlgebra.FinsuppVectorSpace (#3294)
Added Finsupp.coe_basisSingleOneView on Github →