transpose_replicateCol — Mathlib

English

The transpose of the replicated column matrix equals the replicated row matrix: (replicateCol ι v)ᵀ = replicateRow ι v.

Русский

Транспонирование матрицы с повторёнными столбцами даёт матрицу с повторёнными строками: (replicateCol ι v)ᵀ = replicateRow ι v.

LaTeX

$$$ (\mathrm{replicateCol}\ ι v)^{\mathrm{T}} = \mathrm{replicateRow}\ ι v $$$

Lean4

@[simp]
theorem transpose_replicateCol (v : m → α) : (replicateCol ι v)ᵀ = replicateRow ι v :=
  by
  ext
  rfl

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