Theorems · Definition · group theory

Matrix.SpecialLinearGroup.toGLPos

{n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          [inst_3 : LinearOrder R] →
            [inst_4 : IsStrictOrderedRing R] → Matrix.SpecialLinearGroup n R →* ↥(Matrix.GLPos n R)

Matrix.SpecialLinearGroup n R embeds into GL_pos n R

Defined in: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Cited by: 7 results in Mathlib
Foundations: Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype CommRing LinearOrder IsStrictOrderedRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
CommRingstatement and proof · cited by 17,173
LinearOrderstatement and proof · cited by 8,572
Fintypestatement and proof · cited by 7,736
Matrixstatement · cited by 4,303
MonoidHomstatement · cited by 3,629
Subgroupstatement · cited by 3,593
IsStrictOrderedRingstatement and proof · cited by 2,490
Matrix.GeneralLinearGroupstatement · cited by 556
Matrix.SpecialLinearGroupstatement and proof · cited by 348
Matrix.SpecialLinearGroup.toGLproof · cited by 64
Matrix.GLPosstatement · cited by 16

Cited by10

Results whose statement or proof uses this declaration.

ModularGroup.coeproof · cited by 5
ModularGroup.SLOnGLPosproof · cited by 2
ModularGroup.coeHomproof · cited by 1
Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrixstatement · cited by 0
Matrix.SpecialLinearGroup.coe_GLPos_negstatement · cited by 0
Matrix.SpecialLinearGroup.toGLPos_injectivestatement · cited by 0
Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_detstatement · cited by 0
ModularGroup.coe_oneproof · cited by 0
ModularGroup.SLOnGLPos_smul_applystatement · cited by 0
ModularGroup.SL_to_GL_towerproof · cited by 0