R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : z ∣ x
hy : z ∣ y
⊢ z ∣ gcd x y
rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {gcd x y} ≤ Ideal.span {z}
rw [span_gcd, Ideal.span_insert, sup_le_iff]
no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
x y z : R
hx : Ideal.span {x} ≤ Ideal.span {z}
hy : Ideal.span {y} ≤ Ideal.span {z}
⊢ Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
exact ⟨hx, hy⟩