Theorems · Definition · nonassociative algebras

LieAlgebra.SpecialLinear.single

{n : Type u_1} →
  {R : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → (i j : n) → i ≠ j → R →ₗ[R] ↥(LieAlgebra.SpecialLinear.sl n R)

When i ≠ j, the single-element matrices are elements of sl n R. Along with some elements produced by singleSubSingle, these form a natural basis of sl n R.

Defined in

Mathlib.Algebra.Lie.Classical

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype