# `Set.center`, `Set.centralizer` and the `star` operation #

source
theorem Set.star_mem_center {R : Type u_1} [Mul R] [StarMul R] {a : R} (ha : a ∈ center R) :
star a ∈ center R
source
theorem Set.star_centralizer {R : Type u_1} [Mul R] [StarMul R] {s : Set R} :
star s.centralizer = (star s).centralizer
source
theorem Set.union_star_self_comm {R : Type u_1} [Mul R] [StarMul R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y) (hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y) (x : R) :
x ∈ s ∪ star s → ∀ y ∈ s ∪ star s, y * x = x * y
source
theorem Set.star_mem_centralizer' {R : Type u_1} [Mul R] [StarMul R] {a : R} {s : Set R} (h : ∀ a ∈ s, star a ∈ s) (ha : a ∈ s.centralizer) :
star a ∈ s.centralizer
source
theorem Set.star_mem_centralizer {R : Type u_1} [Mul R] [StarMul R] {a : R} {s : Set R} (ha : a ∈ (s ∪ star s).centralizer) :
star a ∈ (s ∪ star s).centralizer