coe_neg — Mathlib

English

For every g in GLPos(n, R) and every indices i, j, the (i, j) entry of the matrix -g equals the negation of the (i, j) entry of g. In other words, negation is applied entrywise to the matrix representation.

Русский

Для любого g ∈ GL^+(n, R) и любых индексов i, j, элемент (i, j) матрицы -g равен отрицанию элемента (i, j) матрицы g.

LaTeX

$$$\bigl( -g \bigr)_{ij} = -\bigl(g\bigr)_{ij}, \quad \forall i,j.$$$

Lean4

@[simp]
theorem coe_neg (g : GLPos n R) : (↑(-g) : GL n R) = -((g : GL n R) : Matrix n n R) :=
  rfl

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