updateRow — Mathlib

English

For DecidableEq m, and any f : α → β, map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b).

Русский

Для разрешимого сравнения m и отображения f: α → β верно: map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b).

LaTeX

$$$ \mathrm{map}\ (\mathrm{updateRow}\ M\ i\ b)\ f = \mathrm{updateRow}\ (M.map f)\ i\ (f \circ b) $$$

Lean4

/-- Update, i.e. replace the `i`th row of matrix `A` with the values in `b`. -/
def updateRow [DecidableEq m] (M : Matrix m n α) (i : m) (b : n → α) : Matrix m n α :=
  of <| Function.update M i b

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