Test_for_Ideal
Provedidealsproofwikirings
Let J be a subset of a ring R. Then J is an ideal of R iff J is nonempty, closed under subtraction, and absorbs ring multiplication.
Preamble
import Mathlib.RingTheory.Ideal.Basic import Mathlib.Data.Set.Basic
Formal statement
theorem Test_for_Ideal {R : Type _} [Ring R] (J : Set R) (hne : J.Nonempty) (hsub : ∀ x y : R, x ∈ J → y ∈ J → x - y ∈ J) (hmul : ∀ j r : R, j ∈ J → j * r ∈ J ∧ r * j ∈ J) : ∃ (I : Ideal R), (↑I : Set R) = J := by sorrySource