Centers of rings

@[simp]

theorem Set.natCast_mem_center (M : Type u_1) [NonAssocSemiring M] (n : ℕ) : ↑n ∈ Set.center M

@[simp]

theorem Set.ofNat_mem_center (M : Type u_1) [NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n ∈ Set.center M

@[simp]

theorem Set.intCast_mem_center (M : Type u_1) [NonAssocRing M] (n : ℤ) : ↑n ∈ Set.center M

@[simp]

theorem Set.add_mem_center {M : Type u_1} [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a + b ∈ Set.center M

@[simp]

theorem Set.neg_mem_center {M : Type u_1} [NonUnitalNonAssocRing M] {a : M} (ha : a ∈ Set.center M) : -a ∈ Set.center M