transpose_replicateRow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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