English
If I and J are primary and have equal radicals, then I ∩ J is primary.
Русский
Если I и J — примарные и радикалы равны, то I ∩ J примарен.
LaTeX
$$$(I \\cap J).IsPrimary \\leftarrow (I.IsPrimary \\land J.IsPrimary \\land \\sqrt{I} = \\sqrt{J}).$$$
Lean4
theorem isPrimary_inf {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary) (hij : radical I = radical J) :
(I ⊓ J).IsPrimary :=
isPrimary_iff.mpr
⟨ne_of_lt <| lt_of_le_of_lt inf_le_left (lt_top_iff_ne_top.2 hi.1), fun {x y} ⟨hxyi, hxyj⟩ =>
by
rw [radical_inf, hij, inf_idem]
rcases (isPrimary_iff.mp hi).2 hxyi with hxi | hyi
· rcases (isPrimary_iff.mp hj).2 hxyj with hxj | hyj
· exact Or.inl ⟨hxi, hxj⟩
· exact Or.inr hyj
· rw [hij] at hyi
exact Or.inr hyi⟩
