traceForm_apply_apply — Mathlib

English

The trace form on a Lie module M, associated to a finite free representation, yields a bilinear form on the Lie algebra L; it is constructed via trace of the representation φ: L → End_R(M).

Русский

Следовая форма на Ли-модуле M, связанная с конечной свободной представительной парой, задаёт билинейную форму на алгебру Ли L; она определяется как след отображения φ: L → End_R(M).

LaTeX

$$$$ \text{traceForm} : L \times L \to R, \quad \text{traceForm}(x,y) = \operatorname{trace}(\phi(x) \circ \phi(y)) $$$$

Lean4

theorem traceForm_apply_apply (x y : L) : traceForm R L M x y = trace R _ (φ x ∘ₗ φ y) :=
  rfl

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