Theorem: update_nz_0 (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝¹ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝ : Semiring R
d : DecidableEq (Fin (n + 1))
f : Fin (n + 1) → A
x : A
i : Fin (n + 1)
i0 : i ≠ 0
⊢ Function.update f i x 0 = f 0
Tactic:
rw [Function.update_noteq i0.symm]
State after:
no goals