Subring_Test
Provedproofwikiringssubrings
Let S be a subset of a ring R. Then S is a subring iff S is nonempty, closed under subtraction, and closed under multiplication.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subring_Test {R : Type _} [Ring R] (S : Subring R) (x y : R) (hx : x ∈ S) (hy : y ∈ S) : x - y ∈ S ∧ x * y ∈ S := by sorrySource