Stream: new members

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.

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

Aah, yes, that's a "bug"

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

It should only ask that for i \in s

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

Ah ok, I was wondering why this assumption.

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

sorry, I meant i \in t

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

I will correct it

#4506

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

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

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

@Riccardo Brasca In fact, both hypotheses were too string

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

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

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

I am used only to tactics

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

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

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