fromCols_neg — Mathlib

English

Negating a matrix partitioned by columns is the same as negating each of the column blocks: -fromCols(A1,A2) = fromCols(-A1,-A2).

Русский

Отрицание матрицы, разбиенной по столбцам, равно отрицанию каждого столбцового блока: -fromCols(A1,A2) = fromCols(-A1,-A2).

LaTeX

$$$$ -\operatorname{fromCols}(A_1,A_2) = \operatorname{fromCols}(-A_1)(-A_2). $$$$

Lean4

/-- Negating a matrix partitioned by columns is equivalent to negating each of the columns. -/
@[simp]
theorem fromCols_neg (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) : -fromCols A₁ A₂ = fromCols (-A₁) (-A₂) := by
  ext i (j | j) <;> simp

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