sl — Mathlib · SciLib

English

The special linear Lie algebra sl_n(R) is the set of all n×n matrices with trace zero, forming a Lie subalgebra of M_n(R).

Русский

Специальная линейная алгебра Ли sl_n(R) состоит из матриц n×n с нулевой следой и образует подалгебру Ли внутри M_n(R).

LaTeX

$$$$ \mathrm{sl}_n(R) = \{ A \in \mathrm{Mat}_{n}(R) \mid \operatorname{tr}(A)=0 \} = \ker(\operatorname{trace}). $$$$

Lean4

/-- The special linear Lie algebra: square matrices of trace zero. -/
def sl [Fintype n] : LieSubalgebra R (Matrix n n R) :=
  { LinearMap.ker (Matrix.traceLinearMap n R R) with
    lie_mem' := fun _ _ => LinearMap.mem_ker.2 <| matrix_trace_commutator_zero _ _ _ _ }

Похожие утверждения