English
The center of a direct product equals the product of centers: center(M × N) = center(M) ×ˢ center(N).
Русский
Центр прямого произведения равен произведению центров: center(M × N) = center(M) ×ˢ center(N).
LaTeX
$$$ \mathrm{center}(M \times N) = \mathrm{center}(M) \times\!\mathrm{center}(N) $$$
Lean4
@[to_additive addCenter_prod]
theorem center_prod {N : Type*} [Mul N] : center (M × N) = center M ×ˢ center N :=
by
ext x
simp only [mem_prod, mem_center_iff, isMulCentral_iff, commute_iff_eq, Prod.ext_iff]
exact
⟨fun ⟨h1, h2, h3⟩ =>
⟨⟨fun a => (h1 (a, x.2)).1, fun b c => (h2 (b, x.2) (c, x.2)).1, fun a b => (h3 (a, x.2) (b, x.2)).1⟩,
⟨fun a => (h1 (x.1, a)).2, fun a b => (h2 (x.1, a) (x.1, b)).2, fun a b => (h3 (x.1, a) (x.1, b)).2⟩⟩,
fun ⟨⟨h1, h2, h3⟩, ⟨h4, h5, h6⟩⟩ =>
⟨fun _ => ⟨h1 _, h4 _⟩, fun _ _ => ⟨h2 _ _, h5 _ _⟩, fun _ _ => ⟨h3 _ _, h6 _ _⟩⟩⟩
