prod_equivMapDomain — Mathlib

English

The product over β of the mapped domain equals the product over α of the original domain transported by f: prod (equivMapDomain f l) g = prod l (λ a m, g (f a) m).

Русский

Произведение по β от образованной области равно произведению по α от исходного с учётом переноса через f.

LaTeX

$$prod (equivMapDomain f l) g = prod l (fun a m => g (f a) m)$$

Lean4

@[to_additive (attr := simp)]
theorem prod_equivMapDomain [CommMonoid N] (f : α ≃ β) (l : α →₀ M) (g : β → M → N) :
    prod (equivMapDomain f l) g = prod l (fun a m => g (f a) m) := by simp [prod, equivMapDomain]

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