Set.center, Set.centralizer and the star operation

theorem Set.star_mem_center {R : Type u_1} [Mul R] [StarMul R] {a : R} (ha : a ∈ Set.center R) : star a ∈ Set.center R

theorem Set.star_centralizer {R : Type u_1} [Mul R] [StarMul R] {s : Set R} : star s.centralizer = (star s).centralizer

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

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

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