Theorems · Definition · group theory

Matrix.SpecialLinearGroup.mapGL

{n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] →
          (S : Type u_1) → [inst_3 : CommRing S] → [Algebra R S] → Matrix.SpecialLinearGroup n R →* GL n S

mapGL is the map from the special linear group over R to the general linear group over S, where S is an R-algebra.

Defined in

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Cited by

98 results in Mathlib

Foundations

Depth 107 from the axioms, rests on 3,214 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRingCommRingAlgebra