English
A proper ideal I is primary if and only if I ≠ ⊤ and for all x,y in R, xy ∈ I implies x ∈ I or y ∈ radical(I).
Русский
Правильный (примарный) идеал I точно не равен R и выполняется: для всех x,y ∈ R, если xy ∈ I, то x ∈ I или y ∈ радикал(I).
LaTeX
$$$I^{}IsPrimary \\iff I \\neq \\top \\land \\forall x,y:\\; x y \\in I \\rightarrow x \\in I \\lor y \\in \\sqrt{I}.$$$
Lean4
/-- A proper ideal `I` is primary iff `xy ∈ I` implies `x ∈ I` or `y ∈ radical I`. -/
theorem isPrimary_iff {I : Ideal R} : I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ radical I :=
by
rw [IsPrimary, Submodule.IsPrimary, forall_comm]
simp only [mul_comm, mem_radical_iff, ← Submodule.ideal_span_singleton_smul, smul_eq_mul, mul_top,
span_singleton_le_iff_mem]
