HepLean Documentation

Mathlib.Algebra.Ring.Center

Centers of rings #

source
@[simp]
theorem Set.natCast_mem_center (M : Type u_1) [NonAssocSemiring M] (n : ℕ) :
↑n ∈ Set.center M
source
@[simp]
theorem Set.ofNat_mem_center (M : Type u_1) [NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] :
OfNat.ofNat n ∈ Set.center M
source
@[simp]
theorem Set.intCast_mem_center (M : Type u_1) [NonAssocRing M] (n : ℤ) :
↑n ∈ Set.center M
source
@[simp]
theorem Set.add_mem_center {M : Type u_1} [Distrib M] {a : M} {b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
a + b ∈ Set.center M
source
@[simp]
theorem Set.neg_mem_center {M : Type u_1} [NonUnitalNonAssocRing M] {a : M} (ha : a ∈ Set.center M) :
-a ∈ Set.center M