English
For a two-argument operator op i x y with op i 1 1 = 1 for all i, mulSingle i (op i x y) equals the function j ↦ op j (mulSingle i x j) (mulSingle i y j).
Русский
Для двухаргументного оператора op i x y с условием op i 1 1 = 1 выполняется mulSingle i (op i x y) = λ j, op j (mulSingle i x j) (mulSingle i y j).
LaTeX
$$$(\forall i, x y,\; mulSingle i (op i x y) = λ j, op j (mulSingle i x j) (mulSingle i y j))$$$
Lean4
@[to_additive]
theorem mulSingle_op₂ (op : ∀ i, M i → N i → O i) (h : ∀ i, op i 1 1 = 1) (i : ι) (x : M i) (y : N i) :
mulSingle i (op i x y) = fun j ↦ op j (mulSingle i x j) (mulSingle i y j) :=
.symm <| funext <| apply_mulSingle₂ op h i x y
