Zulip Chat Archive

Stream: new members

Topic: Confusion about a finset


view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:22):

Hi all. I have a finite set SRS \subset R of elements in a ring RR that are pairwise coprime and such that any element xSx \in S divides a fixed element zRz \in R. It seems that there is already a lemma that says exactly this in ring_theory.coprime: fintype.prod_dvd_of_coprime. So far so good, but I have problems in using it. The point is that in my code SS is implemented as a S : finset R but the lemma requires a type (S : Type) [fintype I]. Is there a way to convert a finset to a fintype?

Note that there is also finset.prod_dvd_of_coprime , but it seems less suited to my situation.

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:23):

Hmm, what does finset.prod_dvd_of_coprime say? Let me check it

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:23):

Because that would have been my first guess

view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:24):

Ah, I just found finset_coe.fintype that maybe is what I need.

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:25):

Yes, but if you can avoid the coe that might be even better

view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:25):

The problem with finset.prod_dvd_of_coprimeis that it needs a type I : Type and a function s : I → R
such that ∀ (i : I), s i ∣ z). I can use R for the type I and id : R \r R as function, but then the assumption ∀ (i : I), s i ∣ z) is not true.

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:26):

Aah, yes, that's a "bug"

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:26):

It should only ask that for i \in s

view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:26):

Ah ok, I was wondering why this assumption.

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:27):

sorry, I meant i \in t

view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:38):

I will correct it

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:51):

#4506

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:51):

Ooh, sorry, I didn't see that you were working on it

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:51):

@Riccardo Brasca In fact, both hypotheses were too string

view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:51):

Don't worry :) The proof is rather mysterious for me

view this post on Zulip Riccardo Brasca (Oct 07 2020 at 13:52):

I am used only to tactics

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:52):

Yeah, it's one of those compact term mode proofs

view this post on Zulip Johan Commelin (Oct 07 2020 at 13:52):

Took me a long time to understand how to decipher them


Last updated: May 18 2021 at 15:14 UTC