R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
⊢ radical (I * J) ≤ radical I ⊓ radical J
R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
⊢ radical (I * J) = radical I ⊓ radical J
refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
  ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩
R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
this : radical (I * J) ≤ radical (I ⊓ J)
⊢ radical (I * J) ≤ radical I ⊓ radical J
R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
⊢ radical (I * J) ≤ radical I ⊓ radical J
have := radical_mono <| @mul_le_inf _ _ I J
R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
this : radical (I * J) ≤ radical I ⊓ radical J
⊢ radical (I * J) ≤ radical I ⊓ radical J
R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
this : radical (I * J) ≤ radical (I ⊓ J)
⊢ radical (I * J) ≤ radical I ⊓ radical J
simp_rw [radical_inf I J] at this
no goals
R : Type u
ι : Type ?u.325271
inst✝ : CommSemiring R
I J K L : Ideal R
this : radical (I * J) ≤ radical I ⊓ radical J
⊢ radical (I * J) ≤ radical I ⊓ radical J
assumption