mathlib
53dc7ca3 - feat(linear_algebra/basic): some basic lemmas about dfinsupp.sum (#12214)

Commit

4 years ago

feat(linear_algebra/basic): some basic lemmas about dfinsupp.sum (#12214) Two basic lemmas about dfinsupp.sum that could be useful (I needed them for another project)

Author

pbazin

Parents

052d027f

mathlib 53dc7ca3 - feat(linear_algebra/basic): some basic lemmas about dfinsupp.sum (#12214)

mathlib
53dc7ca3 - feat(linear_algebra/basic): some basic lemmas about dfinsupp.sum (#12214)