English
For DecidableEq n, (f : α → β) satisfies map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c).
Русский
Для DecidableEq n: map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c).
LaTeX
$$$ \mathrm{map}\ (\mathrm{updateCol}\ M\ j\ c)\ f = \mathrm{updateCol}\ (M.map f)\ j (f \circ c) $$$
Lean4
theorem map_updateCol [DecidableEq n] (f : α → β) : map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c) :=
by
ext
rw [updateCol_apply, map_apply, map_apply, updateCol_apply]
exact apply_ite f _ _ _