mathlib
33694ffd - chore(data/finsupp/defs): move lemmas out of the single section which are not about single (#18260)

Commit
2 years ago
chore(data/finsupp/defs): move lemmas out of the single section which are not about single (#18260)
Author
Parents
Loading