mathlib3
955890d3 - chore(data/finset): remove unused imports (#17891)

Commit

3 years ago

chore(data/finset): remove unused imports (#17891) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

astrainfinita

Parents