doc(data/dfinsupp): improve the docstring for dfinsupp (#15554)
doc(data/dfinsupp): improve the docstring for dfinsupp (#15554)

This adds a brief comment about notation, and an extended implementation note.





leanprover-community/mathlib,leanprover-community/mathlib