data.fintype.basic

Stream: general

[Scott Morrison]

data.fintype.basic has become a giant grab bag of things mentioning fintype. Would anyone like to have a go at carving pieces off it?

That and logic.equiv.basic (much lower down in the hierarchy) are two of the more conspicuous bottlenecks in the import graph at the moment.

[Floris van Doorn]

file#data/fintype/basic
file#logic/equiv/basic

[Scott Morrison]

I split file#logic/equiv/basic a bit in #17038.