transpose — Mathlib

English

If M is block triangular with respect to b, then its transpose is block triangular with respect to the labeling toDual ∘ b.

Русский

Если M блочно-треугольна относительно b, то её транспонированная матрица блочно-треугольна относительно разметки toDual ∘ b.

LaTeX

$$$\BlockTriangular M\; b \Rightarrow \BlockTriangular\bigl(M^{\top}\bigr)\bigl(toDual \circ b\bigr)$$$

Lean4

protected theorem transpose : M.BlockTriangular b → Mᵀ.BlockTriangular (toDual ∘ b) :=
  swap

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