coe_GLPos_neg — Mathlib

English

For g in SpecialLinearGroup, the negation -g, viewed as GLPos, corresponds with the negative of g viewed as GLPos: ↑(-g) = -(↑g).

Русский

Для g ∈ SL(n,R) отрицание -g, рассматриваемое как GLPos, соответствует отрицанию g как элемента GLPos: ↑(-g) = -(↑g).

LaTeX

$$↑(-g) = -(↑g) : GL^+(n,R).$$

Lean4

@[norm_cast]
theorem coe_GLPos_neg (g : SpecialLinearGroup n R) : ↑(-g) = -(↑g : GLPos n R) :=
  Subtype.ext <| Units.ext rfl

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