Zulip Chat Archive

Stream: maths

Topic: two instances of fintype


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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