coe_neg_GL — Mathlib

English

For every g in GLPos(n, R), the image of -g in GL(n, R) equals the negative of the image of g in GL(n, R). In symbols, the natural embedding GLPos(n, R) → GL(n, R) respects negation.

Русский

Пусть g ∈ GL^+(n, R). Образ -g в GL(n, R) равен отрицанию образа g в GL(n, R). То есть натуральное вложение GL^+ в GL сохраняет отрицание.

LaTeX

$$$\bigl( -g \bigr) \text{ viewed in } GL(n,R) = -\bigl( g \text{ viewed in } GL(n,R) \bigr).$$$

Lean4

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

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