neg

Mathlib.Algebra.Lie.Weights.Killing

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

English

There are isomorphisms related to the weight lattice via negative weights forming an involution.

Русский

Существует инволютивное отображение для веса, соответствующее отрицанию.

LaTeX

$$$ \\text{InvolutiveNeg} : Weight \\to Weight $$$

Lean4

theorem neg (h : α.IsZero) : (-α).IsZero := by ext; rw [coe_neg, h, neg_zero]

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

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

Разделы

Аффилиация

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