R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
ha✝ : Irreducible a
ha : maximalIdeal R = span {a}
hb✝ : Irreducible b
hb : maximalIdeal R = span {b}
⊢ Associated a b
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
ha : Irreducible a
hb : Irreducible b
⊢ Associated a b
rw [irreducible_iff_uniformizer] at ha hb
no goals
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
a b : R
ha✝ : Irreducible a
ha : maximalIdeal R = span {a}
hb✝ : Irreducible b
hb : maximalIdeal R = span {b}
⊢ Associated a b
rw [← span_singleton_eq_span_singleton, ← ha, hb]