updateCol — Mathlib

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)

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