English
Let s be a nonempty multiset and f: M → N → O satisfy bilinearity f(a b, c d) = f(a,c) f(b,d) and f(1,1) = 1. Then for f1: ι → M and f2: ι → N, the product of f(f1 i)(f2 i) over i∈s equals the product over i of f1 i and f2 i separately: prod(f(f1 i)(f2 i)) = prod(f1) · prod(f2).
Русский
Пусть s непустое мультимножество и f: M → N → O удовлетворяет билинейности f(ab, cd) = f(a,c) f(b,d) и f(1,1) = 1. Тогда для отображений f1, f2: ι → M, ι → N выполняется равенство произведений: prod(f(f1 i)(f2 i)) = prod(f1) · prod(f2).
LaTeX
$$$ \text{продукт }(\,\mathrm{map}(i \mapsto f(f_1 i)(f_2 i))\, s\,) = f(\mathrm{map} f_1 s).prod (\mathrm{map} f_2\ s).prod $$$
Lean4
@[to_additive]
theorem prod_hom₂_ne_zero [CommMonoid O] {s : Multiset ι} (hs : s ≠ 0) (f : M → N → O)
(hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N) :
(s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod := by
induction s using Quotient.inductionOn; aesop (add simp List.prod_hom₂_nonempty)
