replicateCol_cons — Mathlib

English

Replicating a column vecCons x u yields a matrix whose first column is vecCons x repeated and whose remaining columns follow replicateCol u.

Русский

Повторение столбца vecCons x u даёт матрицу, в которой первый столбец повторяет vecCons x, а оставшиеся столбцы повторяют replicateCol u.

LaTeX

$$$\\mathrm{replicateCol}\\,\\iota\\, (\\mathrm{vecCons}\\, x\\, u) = \\mathrm{of}(\\mathrm{vecCons}(\\lambda\\_ => x)(\\mathrm{replicateCol}\\, \\iota\\, u))$$$

Lean4

@[simp]
theorem replicateCol_cons (x : α) (u : Fin m → α) :
    replicateCol ι (vecCons x u) = of (vecCons (fun _ => x) (replicateCol ι u)) :=
  by
  ext i j
  refine Fin.cases ?_ ?_ i <;> simp

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