English
Let f' be a family of maps with f'i 1 = 1 for all i. Then applying f' after mulSingle distributes pointwise: f' j (mulSingle i x j) = mulSingle i (f' i x) j for all i,x,j.
Русский
Пусть f' — семейство отображений с условием f'i 1 = 1 для всех i. Тогда применение f' к mulSingle распределяется по координатам: f' j (mulSingle i x j) = mulSingle i (f' i x) j для всех i, x, j.
LaTeX
$$$\forall (f' : \forall i, M i \to N i), (\forall i, f' i\, 1 = 1) \to \forall i (x : M i) (j : ι),\; f' j (mulSingle i x j) = mulSingle i (f' i x) j$$$
Lean4
@[to_additive]
theorem apply_mulSingle (f' : ∀ i, M i → N i) (hf' : ∀ i, f' i 1 = 1) (i : ι) (x : M i) (j : ι) :
f' j (mulSingle i x j) = mulSingle i (f' i x) j := by
simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j
