fromRows_neg — Mathlib

English

Negating a matrix partitioned by rows is the same as negating each of the row blocks: the negative of fromRows(A1,A2) equals fromRows(-A1,-A2).

Русский

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

LaTeX

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

Lean4

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

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