English
Let s be a multiset, f : M → N → O be bilinear with f 1 1 = 1. Then for sequences f1, f2: ι → M and ι → N, the bilinear product identity holds: (s.map (f ∘ (f1,f2))).prod = f((s.map f1).prod, (s.map f2).prod).prod
Русский
Пусть s – мультимножество, f: M → N → O удовлетворяет билинейности и f(1,1)=1. Тогда для отображений f1, f2 выполняется тождество: prod(f(f1 i, f2 i)) = f(prod f1, prod f2).
LaTeX
$$$ \prod_{i\in s} f(f_1(i), f_2(i)) = f(\prod_{i\in s} f_1(i), \prod_{i\in s} f_2(i)) $$$
Lean4
@[to_additive]
theorem prod_hom₂ [CommMonoid O] (s : Multiset ι) (f : M → N → O) (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) :
(s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod :=
Quotient.inductionOn s fun l => by simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]
