Null_Ring_and_Ring_Itself_Subrings
Provedproofwikiringssubrings
In any ring R, the null ring and R itself are subrings of R.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Null_Ring_and_Ring_Itself_Subrings {R : Type _} [Ring R] (r : R) : r ∈ (⊤ : Subring R) := by sorrySource