coe_neg_apply — Mathlib

English

The subtype GLPos(n, R) admits a HasDistribNeg structure: for g, h in GLPos(n, R), we have (-g)h = -(gh) and g(-h) = -(gh).

Русский

Подмножество GL^+(n,R) обладает свойством распространённого отрицания: для g, h ∈ GL^+(n,R) выполняются (-g)h = -(gh) и g(-h) = -(gh).

LaTeX

$$$(-g)h = -(gh) \quad\text{and}\quad g(-h) = -(gh), \quad g,h \in GL^+_n(R).$$$

Lean4

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

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