tprod_noncommProd — Mathlib

English

To show two algebra morphisms from a finite PiTensorProduct are equal, it suffices to verify equality on each single-factor embedding (singleAlgHom).

Русский

Чтобы доказать равенство двух алгебра-гомоморфизмов из конечного PiTensorProduct, достаточно проверить их равенство на каждого вложения-одиночки (singleAlgHom).

LaTeX

$$$\\text{algHom\\_ext}\\ (f,g)\\ (h_i)$$$

Lean4

@[simp]
theorem tprod_noncommProd {κ : Type*} (s : Finset κ) (x : κ → Π i, A i) (hx) :
    tprod R (s.noncommProd x hx) = s.noncommProd (fun k => tprod R (x k)) (hx.imp fun _ _ => Commute.tprod) :=
  Finset.map_noncommProd s x _ (tprodMonoidHom R)

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