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_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