English
For a family of multiplicative groups A_i indexed by i, the center of the product equals the product of centers: center(Π_i A_i) = ∏_i center(A_i).
Русский
Для семейства мультипликативных групп A_i, индексируемого i, центр произведения равен произведению центров: center(Π_i A_i) = ∏_i center(A_i).
LaTeX
$$$ \mathrm{center}(\prod_i A_i) = \prod_i \mathrm{center}(A_i) $$$
Lean4
@[to_additive addCenter_pi]
theorem center_pi {ι : Type*} {A : ι → Type*} [Π i, Mul (A i)] : center (Π i, A i) = univ.pi (fun i => center (A i)) :=
by
classical
ext x
simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left, commute_iff_eq, funext_iff,
Pi.mul_def]
exact
⟨fun ⟨h1, h2, h3⟩ i =>
⟨fun a => by simpa using h1 (update x i a) i, fun b c => by simpa using h2 (update x i b) (update x i c) i,
fun a b => by simpa using h3 (update x i a) (update x i b) i⟩,
fun h => ⟨fun a i => (h i).1 (a i), fun b c i => (h i).2.1 (b i) (c i), fun a b i => (h i).2.2 (a i) (b i)⟩⟩
