updateCol_subsingleton — Mathlib

English

If n is a Subsingleton, then A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0).

Русский

Если n является подмножество, то A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0).

LaTeX

$$$ A.updateCol i b = (\mathrm{replicateCol}(\mathrm{Fin} 1)\ b).\mathrm{submatrix}\ id\ (\mathrm{Function.const}\ n\ 0) $$$

Lean4

@[simp]
theorem updateCol_subsingleton [Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R) :
    A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0) :=
  by
  ext x y
  simp [Subsingleton.elim i y]

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