Theorems · Definition · group theory

Matrix.ProjGenLinGroup.signDet

{n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] →
          [Fact (Even (Fintype.card n))] →
            [inst_4 : LinearOrder R] → [IsStrictOrderedRing R] → Matrix.ProjGenLinGroup n R →* SignTypeˣ

In case of an even dimension, the sign of the determinant of g : PGL(n, R) is well-defined.

Defined in

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Cited by

2 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqCommRingFactLinearOrderIsStrictOrderedRing