replicateRow_empty — Mathlib

English

The row-wise replication of a zero-length row vecEmpty yields a matrix whose every row is vecEmpty.

Русский

Повторение строки vecEmpty нулевой длины даёт матрицу, у которой каждая строка равна vecEmpty.

LaTeX

$$$\\mathrm{replicateRow}\\, ι\\, (\\mathrm{vecEmpty}) = \\mathrm{of}\\, (\\lambda\\_ => \\mathrm{vecEmpty})$$$

Lean4

@[simp]
theorem replicateRow_empty : replicateRow ι (vecEmpty : Fin 0 → α) = of fun _ => vecEmpty :=
  rfl

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