toLinear_neg

Mathlib.Algebra.Lie.Weights.Killing

URI: https://scilib.ai/kg/mathlib#LieModule.Weight.toLinear_neg

English

If x ∈ L acts nilpotently by adjoint representation, then x=0 under Cartan Killing hypotheses.

Русский

Если элемент x действует нильпотентно через ad, то x=0 при условиях Killing для Cartan.

LaTeX

$$$ x=0 \\text{ if } x \\in H,\\ ad_x \\text{ nilpotent in } L$$$

Lean4

@[simp]
theorem toLinear_neg {α : Weight K H L} : (-α).toLinear = -α.toLinear :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru