fromBlocks_neg — Mathlib

English

Negation distributes over blocks: -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D).

Русский

Отрицание распределяется по блокам: -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D).

LaTeX

$$$ -\\text{fromBlocks } A B C D = \\text{fromBlocks }(-A) (-B) (-C) (-D) $$$

Lean4

theorem fromBlocks_neg [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix o l R) (D : Matrix o m R) :
    -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D) :=
  by
  ext i j
  cases i <;> cases j <;> simp [fromBlocks]

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