Stream: maths

Topic: two instances of fintype

Casper Putz (Jan 18 2019 at 12:07):

Hi, I have the following code where I explicitely constructed an equivalence between two types α and β → γ, and all types are fintypes. I want to conclude that α.card = γ.card ^ β.card but I have a problem with instances. I would like to something like this:

import data.fintype
open fintype

variables {α : Type*} {β : Type*} {γ : Type*}
variables [fintype α] [fintype β] [fintype γ]
variables [decidable_eq α]
variables (f : α ≃ (β → γ))

example : card α = card γ ^ card β :=
calc card α = @card (β → γ) (of_equiv α f) : eq.symm $of_equiv_card f ... = card γ ^ card β : card_fun  The problem is I have two different instances of fintype (β → γ) . The one coming from fintype.of_equiv (which of_equiv_card uses) and one coming from pi.fintype (which card_fun uses). How could I solve this? Or should I try a completely different route? Chris Hughes (Jan 18 2019 at 12:14): Something like this? example : card α = card β ^ card γ := calc card α = @card (β → γ) (of_equiv α f) : eq.symm$ of_equiv_card f
... = card (β → γ) : by congr
... = card γ ^ card β : card_fun


Casper Putz (Jan 18 2019 at 12:23):

Yes! I also needed [decidable_eq β], but then it worked :). Thanks!

Last updated: May 09 2021 at 10:11 UTC