replicateRow_cons — Mathlib

English

Replicating a row vecCons x u yields a matrix whose every row equals vecCons x u.

Русский

Повторение строки vecCons x u даёт матрицу, у которой каждая строка равна vecCons x u.

LaTeX

$$$\\mathrm{replicateRow}\\,ι\\, (\\mathrm{vecCons}\\, x\\, u) = \\mathrm{of}\\; (\\lambda\\_ => \\mathrm{vecCons}\\, x\\, u)$$$

Lean4

@[simp]
theorem replicateRow_cons (x : α) (u : Fin m → α) : replicateRow ι (vecCons x u) = of fun _ => vecCons x u :=
  rfl

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