theorem Set.center_prod {A : Type u_1} {B : Type u_2} [Semigroup A] [Semigroup B] : Set.center (A × B) = Set.center A ×ˢ Set.center B

theorem Set.center_pi {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Semigroup (A i)] [DecidableEq ι] : Set.center ((i : ι) → A i) = Set.univ.pi fun (i : ι) => Set.center (A i)