Documentation

Monlib.Preq.Set

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