isNonZero_neg

Mathlib.Algebra.Lie.Weights.Killing

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

English

Negation preserves nonzeroness of weights under triangulability assumptions.

Русский

Отрицание сохраняет ненулевой вес при треугольности.

LaTeX

$$$ isNonZero(-α) \\Leftrightarrow isNonZero(α) $$$

Lean4

@[simp]
theorem isNonZero_neg {α : Weight K H L} : (-α).IsNonZero ↔ α.IsNonZero :=
  isZero_neg.not

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

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

Разделы

Аффилиация

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