English
For nonempty sets S ⊆ M and T ⊆ N, the centralizer of the product S ×ˢ T equals the product of centralizers: (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer.
Русский
Для непустых множеств S ⊆ M и T ⊆ N централизатор произведения S × T равен произведению централизаторов: (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer.
LaTeX
$$$ (S \times\!\! T).centralizer = S.centralizer \times\!\! T.centralizer $$$
Lean4
/-- The centralizer of the product of non-empty sets is equal to the product of the centralizers. -/
@[to_additive addCentralizer_prod]
theorem centralizer_prod {N : Type*} [Mul N] {S : Set M} {T : Set N} (hS : S.Nonempty) (hT : T.Nonempty) :
(S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer :=
by
ext
simp_rw [mem_prod, mem_centralizer_iff, mem_prod, and_imp, Prod.forall, Prod.mul_def, Prod.eq_iff_fst_eq_snd_eq]
obtain ⟨b, hb⟩ := hS
obtain ⟨c, hc⟩ := hT
exact ⟨fun h => ⟨fun y hy => (h y c hy hc).1, fun y hy => (h b y hb hy).2⟩, fun h y z hy hz => ⟨h.1 _ hy, h.2 _ hz⟩⟩
