updateRow_apply — Mathlib

English

For Finite m, Mul α and AddCommMonoid α, v,w: m → α, replicateRow ι v * replicateCol ι w = of fun _ _ => v ⬝ᵥ w.

Русский

Для Finite m, Mul α, AddCommMonoid α; v,w: m → α; произведение replicateRow ι v и replicateCol ι w даёт константную матрицу со значением v ⬝ᵥ w.

LaTeX

$$$ \mathrm{replicateRow}\ ι\ v * \mathrm{replicateCol}\ ι\ w = \mathrm{of} \; (\lambda _ _ => v ⬝ᵥ w) $$$

Lean4

theorem updateRow_apply [DecidableEq m] {i' : m} : updateRow M i b i' j = if i' = i then b j else M i' j :=
  by
  by_cases h : i' = i
  · rw [h, updateRow_self, if_pos rfl]
  · rw [updateRow_ne h, if_neg h]

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