English
Let GLPos(n, R) denote invertible n×n matrices over a commutative ring R with positive determinant. If n is finite and its cardinality is even, GLPos(n, R) is closed under negation: for every g in GLPos(n, R), -g also lies in GLPos(n, R). In particular, det(-g) = det(g) > 0 since (-1)^{|n|} = 1 for even |n|.
Русский
Пусть GLPos(n, R) обозначает обратимые матрицы размера n×n над коммутативной кольцо R с положительным детерминантом. Пусть |n| чётно. Тогда GLPos(n, R) замкнуто по отношению к отрицанию: для любого g ∈ GLPos(n, R) имеет место -g ∈ GLPos(n, R). В частности, det(-g) = det(g) > 0, так как (-1)^{|n|} = 1.
LaTeX
$$$\forall g \in GL^+_n(R), -g \in GL^+_n(R).$$$
Lean4
/-- Formal operation of negation on general linear group on even cardinality `n` given by negating
each element. -/
instance : Neg (GLPos n R) :=
⟨fun g =>
⟨-g,
by
rw [mem_glpos, GeneralLinearGroup.val_det_apply, Units.val_neg, det_neg,
(Fact.out (p := Even <| Fintype.card n)).neg_one_pow, one_mul]
exact g.prop⟩⟩
