Centralizer_of_Ring_Subset_is_Subring
Provedcentralizersproofwikiringssubrings
The centralizer of a subset of a ring is a subring.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Centralizer_of_Ring_Subset_is_Subring {R : Type _} [Ring R] (s : R) (a b : R) (ha : a * s = s * a) (hb : b * s = s * b) : (a + b) * s = s * (a + b) := by sorrySource