Zulip Chat Archive

Stream: new members

Topic: Confusion about a finset

Riccardo Brasca (Oct 07 2020 at 13:22):

Hi all. I have a finite set $S \subset R$ of elements in a ring $R$ that are pairwise coprime and such that any element $x \in S$ divides a fixed element $z \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 $S$ 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.

Johan Commelin (Oct 07 2020 at 13:23):

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

Johan Commelin (Oct 07 2020 at 13:23):

Because that would have been my first guess

Riccardo Brasca (Oct 07 2020 at 13:24):

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

Johan Commelin (Oct 07 2020 at 13:25):

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

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.