Prop-valued "I am a finite type"

Stream: Is there code for X?

[Kevin Buzzard]

Is it just set.finite (set.univ : set X)? Does this concept deserve its own definition and API? Or nonempty (fintype X)? Which is preferred?

[Kevin Buzzard]

From algebra.big_operators.finprod:

We did not add `is_finite (X : Type) : Prop`, because it is simply `nonempty (fintype X)`.

Git blame says I wrote this. Meh.

[Johan Commelin]

I think @Yury G. Kudryashov announced that he wanted to add this class.