blockTriangular_transpose_iff — Mathlib

English

A matrix Mᵀ is block triangular with respect to b if and only if M is block triangular with respect to the dual labeling of b.

Русский

Транспонированная матрица Mᵀ блочно-треугольна по отношению к b тогда и только тогда, когда M блочно-треугольна по отношению к обратной (dual) разметке.

LaTeX

$$$M^{\top}.BlockTriangular\; b \iff M.BlockTriangular\; (ofDual \circ b)$$$

Lean4

@[simp]
protected theorem blockTriangular_transpose_iff {b : m → αᵒᵈ} : Mᵀ.BlockTriangular b ↔ M.BlockTriangular (ofDual ∘ b) :=
  forall_swap

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