English
Let l be a list and f: M→N→P with bilinear-like property hf and hf' : f 1 1 = 1. Then for any f1: ι→M, f2: ι→N, (l.map (i ↦ f (f1 i) (f2 i))).prod = f (l.map f1).prod (l.map f2).prod.
Русский
Пусть l — список, f: M→N→P обладает свойством билинейности hf и hf' : f 1 1 = 1; тогда для любых 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₂ (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1)
(f₁ : ι → M) (f₂ : ι → N) : (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by
rw [prod, prod, prod, foldr_map, foldr_map, foldr_map, ←
l.foldr_hom₂ f _ _ (fun x y => f (f₁ x) (f₂ x) * y) _ _ (by simp [hf]), hf']
