mathlib
72e0e9a5 - doc(data/dfinsupp): improve the docstring for dfinsupp (#15554)

Commit

3 years ago

doc(data/dfinsupp): improve the docstring for dfinsupp (#15554) This adds a brief comment about notation, and an extended implementation note.

Author

eric-wieser

Parents