Documentation

Mathlib.Algebra.Ring.Centralizer

Centralizers of rings #

@[simp]
theorem Set.add_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [Distrib M] (ha : a S.centralizer) (hb : b S.centralizer) :
a + 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) :
-a S.centralizer