R S : Type u
x y : R
inst✝ : CommSemiring R
⊢ (∀ (p : Submodule R R), p ∈ {J | Ideal.IsPrime J} → x ∈ p) ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J
R S : Type u
x y : R
inst✝ : CommSemiring R
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J
rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]
no goals
R S : Type u
x y : R
inst✝ : CommSemiring R
⊢ (∀ (p : Submodule R R), p ∈ {J | Ideal.IsPrime J} → x ∈ p) ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J
rfl