Theorems · Theorem · nonassociative algebras

LieAlgebra.SpecialLinear.val_single

∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (h : i ≠ j)
  (r : R), ↑((LieAlgebra.SpecialLinear.single i j h) r) = Matrix.single i j r

Defined in

Mathlib.Algebra.Lie.Classical

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype