Theorems · Definition · group theory

Matrix.SpecialLinearGroup.map

{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] → (R →+* S) → Matrix.SpecialLinearGroup n R →* Matrix.SpecialLinearGroup n S

A ring homomorphism from R to S induces a group homomorphism from SpecialLinearGroup n R to SpecialLinearGroup n S.

Defined in

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Cited by

77 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommRingCommRing