update_eq_div_mul_mulSingle — Mathlib

English

For every i, and any g : ∀ i, f i and x ∈ f i, the update of g at i by x equals g divided by mulSingle i (g i) times mulSingle i x.

Русский

Для каждого i и функции g: I → f i с некоторым x ∈ f i, обновление g в позиции i на x равно g делённому на mulSingle i (g i), умноженному на mulSingle i x.

LaTeX

$$$\mathrm{update}\, g\, i\, x = g \; /\; \mathrm{mulSingle}_i(g(i)) \; *\; \mathrm{mulSingle}_i(x)$$$

Lean4

@[to_additive]
theorem update_eq_div_mul_mulSingle [∀ i, Group <| f i] (g : ∀ i : I, f i) (x : f i) :
    Function.update g i x = g / mulSingle i (g i) * mulSingle i x :=
  by
  ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [Function.update_of_ne h.symm, h]

Похожие утверждения