prod_embDomain — Mathlib

English

Replacing the domain by an embedding does not change the product up to the corresponding reindexing.

Русский

Замена домена вложением не изменяет произведение, кроме как за счёт правильной переиндексации.

LaTeX

$$$$ (v.embDomain f).prod g = v.prod (\lambda a b, g (f a) b). $$$$

Lean4

@[to_additive]
theorem prod_embDomain [Zero M] [CommMonoid N] {v : α →₀ M} {f : α ↪ β} {g : β → M → N} :
    (v.embDomain f).prod g = v.prod fun a b => g (f a) b :=
  by
  rw [prod, prod, support_embDomain, Finset.prod_map]
  simp_rw [embDomain_apply]

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