English
Let n be a finite index set of even cardinality and R a commutative ring. For every g in SL(n, R), the matrix -g also lies in SL(n, R); equivalently, det(-g) = 1 for all g ∈ SL(n, R).
Русский
Пусть n - конечный индексный множитель и R - коммутативное кольцо. Для любого g ∈ SL(n, R) матрица -g также принадлежит SL(n, R); эквивалентно, det(-g) = 1 для всех g ∈ SL(n, R).
LaTeX
$$$\forall n,R,g\,(g \in SL(n,R) \Rightarrow -g \in SL(n,R))$, где $n$ имеет чётную кардинальность, и det$(-g)=1$.$$
Lean4
/-- Formal operation of negation on special linear group on even cardinality `n` given by negating
each element. -/
instance instNeg : Neg (SpecialLinearGroup n R) :=
⟨fun g => ⟨-g, by simpa [(@Fact.out <| Even <| Fintype.card n).neg_one_pow, g.det_coe] using det_smul (↑ₘg) (-1)⟩⟩
