coeff_update_ne — Mathlib

English

If a' is different from a, the coefficient at a' in the updated element equals the original coefficient at a'.

Русский

Если a' не равен a, коэффициент при a' в обновленном элементе равен исходному коэффициенту при a'.

LaTeX

$$$\\text{If } a' \\neq a:\\ (f.update\\ a\\ b).\\text{coeff}(a') = f.\\text{coeff}(a').$$$

Lean4

@[simp]
theorem coeff_update_ne (h : a' ≠ a) : (f.update a b).coeff a' = f.coeff a' := by
  classical rw [f.coeff_update_apply, if_neg h]

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