Choose multiples outside of an ideal

Stream: Is there code for X?

[Anne Baanen]

I have a finite collection of nonzero elements f : ι → R and a prime, or at least non-1, ideal p. Do we have a way to find f' : ι → R such that not all f' i are in p, and a * f' i = b * f i for some a, b? Do we have this where f actually goes to the field of fractions of R?

I remember we had something along these lines. Perhaps I'm thinking docs#fractional_ideal.exists_not_mem_one_of_ne_bot does more than it actually did...

[Johan Commelin]

I don't recognize this

[Kevin Buzzard]

If $\iota=\{0,1\}$, $R=\R[X,Y]$, $f(0)=X$ and $f(1)=Y$, and $p=(X,Y)$, then you want to find $a,b$ with $a|bX$ and $a|bY$, and these imply $a|b$ meaning that both $f'(i)\in p$.