English
For DecidableEq n, (f : α → β) maps updateCol M j c to the updateCol of M.map f with j and 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
/-- Update, i.e. replace the `j`th column of matrix `A` with the values in `b`. -/
def updateCol [DecidableEq n] (M : Matrix m n α) (j : n) (b : m → α) : Matrix m n α :=
of fun i => Function.update (M i) j (b i)