IsRelPrime a b →IsRelPrime (Ideal.span {a}) (Ideal.span {b})

Stream: Is there code for X?

[Daniel Weber]

Is there any version of IsRelPrime a b → IsRelPrime (Ideal.span {a}) (Ideal.span {b}) in Mathlib? What are the necessary assumptions for it to hold? I can prove it assuming IsBezout:

import Mathlib

variable (R : Type*) [CommRing R] [IsBezout R]

example (a b : R) (h : IsRelPrime a b) : IsRelPrime (Ideal.span {a}) (Ideal.span {b}) :=
  Ideal.isCoprime_span_singleton_iff a b |>.mpr h.isCoprime |>.isRelPrime

but are there weaker assumptions which suffice?

[Kevin Buzzard]

It's not true for Dedekind domains ($2$ and $1+\sqrt{-5}$ are coprime as numbers, but the principal ideals they generate are both contained in the ideal generated by both of them, which isn't a unit) and it's not true for higher-dimensional rings ($X$ and $Y$ are relatively prime as elements of $\mathbb{C}[X,Y]$ but the ideal they generate isn't all of $\mathbb{C}[X,Y]$) so I'm struggling to see a natural generalisation.

[Kevin Buzzard]

In fact it would not surprise me if this property implied Bezout, at least for integral domains. Or was pretty close to it.