English
Let L be a Lie algebra acting on a finite-dimensional vector space M. If the trace of the endomorphism corresponding to every element x in a subset S is zero, then the trace vanishes on every element of the Lie span of S.
Русский
Пусть L — алгебра Ли, действующая на конечномерное пространство M. Если след соответствующего отображения для каждого элемента x из S равен нулю, то след равен нулю и на всех элементов Lie-порожденной подалгебры от S.
LaTeX
$$$\forall S \subseteq L,\;\Big(\forall x \in S:\; \operatorname{tr}(\mathrm{toEnd}(x)) = 0\Big) \Rightarrow \Big(\forall x \in \mathrm{lieSpan}(S):\; \operatorname{tr}(\mathrm{toEnd}(x)) = 0\Big)$$$
Lean4
theorem trace_toEnd_eq_zero {s : Set L} (hs : ∀ x ∈ s, LinearMap.trace R _ (toEnd R _ M x) = 0) {x : L}
(hx : x ∈ LieSubalgebra.lieSpan R L s) : trace R _ (toEnd R _ M x) = 0 := by
induction hx using LieSubalgebra.lieSpan_induction with
| mem u hu => simpa using hs u hu
| zero => simp
| add u v _ _ hu hv => simp [hu, hv]
| smul t u _ hu => simp [hu]
| lie u v _ _ _ _ => simp
