Ideal_is_Subring
Provedidealsproofwikiringssubrings
Let (R, +, *) be a ring, and let J be an ideal of R. Then J is a subring of R.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Ideal_is_Subring {R : Type _} [CommRing R] (J : Ideal R) (x y : R) (hx : x ∈ J) (hy : y ∈ J) : x - y ∈ J ∧ x * y ∈ J := by sorrySource