blockTriangular_one

Mathlib.LinearAlgebra.Matrix.Block

URI: https://scilib.ai/kg/mathlib#Matrix.blockTriangular_one

English

The identity matrix 1 is block triangular with respect to any labeling b.

Русский

Единичная матрица 1 блочно-треугольна по любой разметке.

LaTeX

$$$\BlockTriangular\bigl(1\bigr)\; b$$$

Lean4

theorem blockTriangular_one [One R] : BlockTriangular (1 : Matrix m m R) b :=
  blockTriangular_diagonal _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru