Theorems · Definition · group theory

Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosedOfNonempty

{n : Type u_1} →
  [inst : Fintype n] →
    [inst_1 : DecidableEq n] →
      [Nonempty n] →
        {F : Type u_3} →
          [inst_3 : Field F] → [IsAlgClosed F] → Matrix.ProjGenLinGroup n F ≃* Matrix.ProjectiveSpecialLinearGroup n F

An isomorphism between PGL(n, F) and PSL(n, F) in the case of an algebraically closed field induced from the natural inclusion map.

Defined in

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNonemptyFieldIsAlgClosed