blockDiag'_neg — Mathlib

English

Let α be an additive group. For any matrix M with entries in α, the block-diagonal extraction operator blockDiag' is compatible with negation: blockDiag'(−M) = − blockDiag'(M).

Русский

Пусть α — аддитивная группа. Для любой матрицы M с элементами в α оператор blockDiag' сохраняет отрицание: blockDiag'(−M) = − blockDiag'(M).

LaTeX

$$$blockDiag'(-M) = - blockDiag'(M)$$$

Lean4

@[simp]
theorem blockDiag'_neg [AddGroup α] (M : Matrix (Σ i, m' i) (Σ i, n' i) α) : blockDiag' (-M) = -blockDiag' M :=
  map_neg (blockDiag'AddMonoidHom m' n' α) M

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