blockDiag'_sub — Mathlib

English

Let α be an additive group. For any matrices M,N of the same size with entries in α, blockDiag'(M − N) = blockDiag'(M) − blockDiag'(N).

Русский

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

LaTeX

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

Lean4

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

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