English
If x lies in the first derived series of L, then χ(x) = 0 for a Lie character χ.
Русский
Пусть x лежит в первой производной последовательности L; тогда для характера χ выполняется χ(x) = 0.
LaTeX
$$$$ x \in \operatorname{derivedSeries}(R,L,1) \Rightarrow \chi(x) = 0. $$$$
Lean4
theorem lieCharacter_apply_of_mem_derived (χ : LieCharacter R L) {x : L} (h : x ∈ derivedSeries R L 1) : χ x = 0 :=
by
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ← LieSubmodule.mem_toSubmodule,
LieSubmodule.lieIdeal_oper_eq_linear_span] at h
refine Submodule.span_induction ?_ ?_ ?_ ?_ h
· rintro y ⟨⟨z, hz⟩, ⟨⟨w, hw⟩, rfl⟩⟩; apply lieCharacter_apply_lie
· exact χ.map_zero
· intro y z _ _ hy hz; rw [LieHom.map_add, hy, hz, add_zero]
· intro t y _ hy; rw [LieHom.map_smul, hy, smul_zero]
