English
Let l be a nonempty list of ι, f: M→N→P with appropriate bilinearity hf, f1: ι→M, f2: ι→N; then (l.map (i ↦ f (f1 i) (f2 i))).prod = f (l.map f1).prod (l.map f2).prod.
Русский
Пусть l — непустой список индексов ι, есть двувзаимная операция f: M→N→P удовлетворяющая билинейности hf, и функции f1,f2. Тогда произведение по элементам равно произведению произведений по обеим факторам.
LaTeX
$$$$ (l.map \\lambda i \\to f (f_1 i) (f_2 i)).prod = f(l.map f_1).prod \\; (l.map f_2).prod. $$$$
Lean4
@[to_additive]
theorem prod_hom₂_nonempty {l : List ι} (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M)
(f₂ : ι → N) (hl : l ≠ []) : (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by
match l, hl with
| x :: xs, hl => induction xs generalizing x <;> simp_all
