tprod_prod — Mathlib

English

The tprod map distributes over finite products: tprod R (∏ k ∈ s, x k) = ∏ k ∈ s, tprod R (x k).

Русский

Карта tprod распределяет над конечными произведениями: tprod R (∏ k ∈ s, x k) = ∏ k ∈ s, tprod R (x k).

LaTeX

$$$tprod\\ R\\ (\\prod k\\in s, x k) = \\prod k\\in s, tprod\\ R\\ (x k)$$$

Lean4

@[simp]
theorem tprod_prod {κ : Type*} (s : Finset κ) (x : κ → Π i, A i) : tprod R (∏ k ∈ s, x k) = ∏ k ∈ s, tprod R (x k) :=
  map_prod (tprodMonoidHom R) x s

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