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