English
If the radical of I is maximal, then I is a primary ideal.
Русский
Если радикал I максимален, то I является первичным идеалом.
LaTeX
$$$I.\mathrm{radical.IsMaximal} \Rightarrow I.\mathrm{IsPrimary}$$$
Lean4
theorem isPrimary_of_isMaximal_radical [CommRing R] {I : Ideal R} (hi : IsMaximal (radical I)) : I.IsPrimary :=
have : radical I = jacobson I :=
le_antisymm (le_sInf fun _ ⟨him, hm⟩ => hm.isPrime.radical_le_iff.2 him) (sInf_le ⟨le_radical, hi⟩)
isPrimary_iff.mpr
⟨ne_top_of_lt <| lt_of_le_of_lt le_radical (lt_top_iff_ne_top.2 hi.1.1), fun {x y} hxy =>
((isLocal_of_isMaximal_radical hi).mem_jacobson_or_exists_inv y).symm.imp
(fun ⟨z, hz⟩ => by
rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]
exact I.sub_mem (I.mul_mem_left _ hxy) (I.mul_mem_left _ hz))
(this ▸ id)⟩
