blockDiagonal'_neg — Mathlib

English

BlockDiagonal' commutes with additive inverses: blockDiagonal'(-M) = - blockDiagonal' M.

Русский

BlockDiagonal' сохраняет противоположности: blockDiagonal'(-M) = - blockDiagonal' M.

LaTeX

$$$ \\mathrm{blockDiagonal}'(-M) = -\\mathrm{blockDiagonal}' M $$$

Lean4

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

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