formulization

Stream: new members

[Alex Zhang]

Is it possible to formulize that for every natural number n, there is a fintype whose card is n?

import data.fintype.card
example : ∀ n : ℕ, ∃ I : Type*, fintype.card I = n

[Bryan Gin-ge Chen]

I was able to find all the proofs using tactic#library_search

import data.fintype.card
example : ∀ n : ℕ, ∃ (I : Type*) (h : fintype I), @fintype.card I h = n :=
λ n, ⟨fin n, fin.fintype n, fintype.card_fin n⟩

[Kevin Buzzard]

That's the second new member question we've had today for which the answer was by library_search :-)

[Bryan Gin-ge Chen]

Ah, actually, I had to know that docs#fin existed too.

[Kevin Buzzard]

Aah yes, you need to know that mathlib has a "canonical" type of size n.