English
Let L' be a Lie subalgebra of L, and let M be a module as above. Then the trace form computed inside L' agrees with the trace form computed inside L when evaluated on corresponding elements of L'. In particular, for any x ∈ L' with hx expressing x ∈ L', and any y ∈ L', the trace form on L' evaluated at ⟨x, hx⟩ and y equals the trace form on L evaluated at x and y.
Русский
Пусть L' ⊆ L — подположение Ли. Пусть M — модуль; тогда форма следа, рассчитанная на L', совпадает с формой следа на L при соответствующих аргументах. Конкретно, для любого x ∈ L' с hx, и любого y ∈ L', имеем traceForm_R,L',M ⟨x, hx⟩ y = traceForm_R,L,M x y.
LaTeX
$$$traceForm R L' M \langle x, hx \rangle y = traceForm R L M x y$$$
Lean4
@[simp]
theorem traceForm_lieSubalgebra_mk_left (L' : LieSubalgebra R L) {x : L} (hx : x ∈ L') (y : L') :
traceForm R L' M ⟨x, hx⟩ y = traceForm R L M x y :=
rfl
