charmatrix_blockTriangular_iff — Mathlib

English

For any matrix M, and any b: n → α with a preorder α, M.charmatrix.BlockTriangular b is equivalent to M.BlockTriangular b.

Русский

Для любой матрицы M и отображения b: n → α с частичным порядком α, charmatrix(M)_BLOCKTriangular b эквивалентна M.BlockTriangular b.

LaTeX

$$$M.\\text{charmatrix.BlockTriangular } b \;\\leftrightarrow\\; M.\\text{BlockTriangular } b$$$

Lean4

@[simp]
theorem charmatrix_blockTriangular_iff {α : Type*} [Preorder α] {M : Matrix n n R} {b : n → α} :
    M.charmatrix.BlockTriangular b ↔ M.BlockTriangular b :=
  by
  rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]
  simp [BlockTriangular]

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