English
Updating the product f1 * f2 at i by x1 * x2 equals updating f1 at i by x1 and f2 at i by x2, then multiplying.
Русский
Обновление произведения f1 * f2 в позиции i на x1 * x2 эквивалентно обновлению f1 в i на x1 и обновлению f2 в i на x2 с последующим перемножением.
LaTeX
$$$\mathrm{update}(f_1 \cdot f_2)\; i\; (x_1 x_2) = \mathrm{update}\, f_1\; i\; x_1 \cdot \mathrm{update}\, f_2\; i\; x_2$$$
Lean4
@[to_additive]
theorem update_mul [∀ i, Mul (f i)] [DecidableEq I] (f₁ f₂ : ∀ i, f i) (i : I) (x₁ : f i) (x₂ : f i) :
update (f₁ * f₂) i (x₁ * x₂) = update f₁ i x₁ * update f₂ i x₂ :=
funext fun j => (apply_update₂ (fun _ => (· * ·)) f₁ f₂ i x₁ x₂ j).symm
