mathlib
27f622ef - chore(data/fintype/basic): split, and reduce imports (#3319)

Commit
5 years ago
chore(data/fintype/basic): split, and reduce imports (#3319) Following on from #3256 and #3235, this slices a little out of `data.fintype.basic`, and reduces imports, mostly in the vicinity of `data.fintype.basic`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
References
Author
Parents
Loading