instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos

English

There is a canonical embedding from the Special Linear group SL(n, R) into GL^+(n, R) given by the natural inclusion, since matrices in SL have determinant 1 and hence positive determinant.

Русский

Существуют канонические вложения из Special Linear Group SL(n, R) в GL^+(n, R) по естественной карте, так как матрицы из SL имеют детерминант 1 и, следовательно, положительный детерминант.

LaTeX

$$$\text{toGLPos}: SL(n,R) \to GL^+_n(R) \text{ is a monoid hom with } A \mapsto A.$$$

Lean4

instance : HasDistribNeg (GLPos n R) :=
  Subtype.coe_injective.hasDistribNeg _ GLPos.coe_neg_GL (GLPos n R).coe_mul

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