blockTriangular_blockDiagonal — Mathlib

English

The blockDiagonal d yields a block triangular matrix with labeling Prod.snd.

Русский

Блок-диагональ d образует блочно-треугольную матрицу относительно Prod.snd.

LaTeX

$$$\BlockTriangular\bigl(\mathrm{blockDiagonal}\; d\bigr)\; \mathrm{Prod}.snd$$$

Lean4

theorem blockTriangular_blockDiagonal [DecidableEq α] (d : α → Matrix m m R) :
    BlockTriangular (blockDiagonal d) Prod.snd :=
  by
  rintro ⟨i, i'⟩ ⟨j, j'⟩ h
  rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']
  exact h

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