R : Type u
ι : Type ?u.271655
inst✝ : CommSemiring R
I J K L : Ideal R
h : I ⊔ K = ⊤
⊢ I ⊔ K * J = I ⊔ J
R : Type u
ι : Type ?u.271655
inst✝ : CommSemiring R
I J K L : Ideal R
h : I ⊔ K = ⊤
⊢ I ⊔ J * K = I ⊔ J
rw [mul_comm]
no goals
R : Type u
ι : Type ?u.271655
inst✝ : CommSemiring R
I J K L : Ideal R
h : I ⊔ K = ⊤
⊢ I ⊔ K * J = I ⊔ J
exact sup_mul_eq_of_coprime_left h