Centralizers of rings #
@[simp]
theorem
Set.add_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[Distrib M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a + b ∈ Set.centralizer S
@[simp]
theorem
Set.neg_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
[Mul M]
[HasDistribNeg M]
(ha : a ∈ Set.centralizer S)
:
-a ∈ Set.centralizer S