head_transpose — Mathlib

English

Taking the head of the transpose-related construction commutes with the transpose operation, i.e., the head of the transposed representation equals the composition of heads with the symmetry.

Русский

Получение головы транспонированной конструкции коммутирует с транспонированием: голова транспонированной формы равна композиции голов со свёрткой.

LaTeX

$$$\\text{head\_transpose}(A) : \\vecHead( A^{\\mathrm{symm}}^{T}) = (\\vecHead \\circ A^{\\mathrm{symm}})$$$

Lean4

@[simp]
theorem head_transpose (A : Matrix m' (Fin n.succ) α) : vecHead (of.symm Aᵀ) = vecHead ∘ of.symm A :=
  rfl

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