traceForm_lieSubalgebra_mk_right — Mathlib

English

Let L' be a Lie subalgebra of L and M a module as above. Then the trace form on L' evaluated at x ∈ L' and ⟨y, hy⟩ ∈ L' (with hy indicating y ∈ L') matches the trace form on L evaluated at x and y. In particular, traceForm R L' M x ⟨y, hy⟩ = traceForm R L M x y.

Русский

Пусть L' ⊆ L — подпалегра. Пусть M — модуль. Тогда traceForm на L', применимая к x ∈ L' и ⟨y, hy⟩ ∈ L' (hy: y ∈ L'), совпадает с traceForm на L, применимой к x и y. То есть traceForm_R,L',M x ⟨y, hy⟩ = traceForm_R,L,M x y.

LaTeX

$$$traceForm R L' M x \langle y, hy \rangle = traceForm R L M x y$$$

Lean4

@[simp]
theorem traceForm_lieSubalgebra_mk_right (L' : LieSubalgebra R L) {x : L'} {y : L} (hy : y ∈ L') :
    traceForm R L' M x ⟨y, hy⟩ = traceForm R L M x y :=
  rfl

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