tail_transpose — Mathlib

English

The tail operator commutes with transpose in the sense that vecTail(of.symm A^T) equals (vecTail ∘ A)^T.

Русский

Хвостовая операция commute с транспонированием: vecTail(of.symm A^T) = (vecTail ∘ A)^T.

LaTeX

$$$\\mathrm{tail\\_transpose}(A) : \\mathrm{vecTail}(\\mathrm{of}.\\mathrm{symm} A^T) = (\\mathrm{vecTail} \\circ A)^T$$$

Lean4

@[simp]
theorem tail_transpose (A : Matrix m' (Fin n.succ) α) : vecTail (of.symm Aᵀ) = (vecTail ∘ A)ᵀ :=
  by
  ext i j
  rfl

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