prod_centralizer_subset_centralizer_prod

English

The product of centralizers is contained in the centralizer of the product: S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer.

Русский

Произведение централизаторов содержится в централизаторе произведения: S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer.

LaTeX

$$$ S.centralizer \times\! T.centralizer \subseteq (S \times\! T).centralizer $$$

Lean4

@[to_additive prod_addCentralizer_subset_addCentralizer_prod]
theorem prod_centralizer_subset_centralizer_prod {N : Type*} [Mul N] (S : Set M) (T : Set N) :
    S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer :=
  by
  rw [subset_def]
  simp only [mem_prod, and_imp, Prod.forall, mem_centralizer_iff, Prod.mk_mul_mk, Prod.mk.injEq]
  exact fun a b ha hb c d hc hd => ⟨ha c hc, hb d hd⟩

Похожие утверждения