case h.e'_1.a
R : Type ?u.702098
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ J * I ≤ J * I' ↔ I * J ≤ I' * J
R : Type ?u.702098
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ J * I ≤ J * I' ↔ I ≤ I'
convert mul_right_le_iff hJ using 1
no goals
case h.e'_1.a
R : Type ?u.702098
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ J * I ≤ J * I' ↔ I * J ≤ I' * J
simp only [mul_comm]