R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type ?u.528557
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : p ∣ q ∨ q ∣ p
⊢ Associated p q
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type ?u.528557
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
⊢ Associated p q
have := dvd_total p q
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type ?u.528557
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type ?u.528557
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : p ∣ q ∨ q ∣ p
⊢ Associated p q
rw [Irreducible.dvd_comm hp hq, or_self_iff] at this
no goals
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
K : Type ?u.528557
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : ValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q
exact associated_of_dvd_dvd (Irreducible.dvd_symm hq hp this) this