traceForm_apply_eq_zero_of_mem_lcs_of_mem_center

English

If x belongs to the lower central series and y to the center, then traceForm(x,y) = 0.

Русский

Если x принадлежит нижнему централному ряду, а y лежит в центре, то traceForm(x,y) = 0.

LaTeX

$$$$ \mathrm{traceForm}(x,y) = 0 \quad\text{for } x \in \text{lcs}, y \in \text{center}. $$$$

Lean4

theorem traceForm_apply_eq_zero_of_mem_lcs_of_mem_center {x y : L} (hx : x ∈ lowerCentralSeries R L L 1)
    (hy : y ∈ LieAlgebra.center R L) : traceForm R L M x y = 0 :=
  by
  apply traceForm_eq_zero_if_mem_lcs_of_mem_ucs R L M 1
  · simpa using hx
  · simpa using hy

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