Theorems · Theorem · group theory

Matrix.SpecialLinearGroup.mem_center_iff

∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  {A : Matrix.SpecialLinearGroup n R},
  A ∈ Subgroup.center (Matrix.SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (Matrix.scalar n) r = ↑A

The center of a special linear group of degree n is the subgroup of scalar matrices, for which the scalars are the n-th roots of unity.

Defined in

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommRing