neg_root_mem

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.neg_root_mem

English

For any i, -P.root i lies in the range of P.root.

Русский

Для любого i, -P.root i лежит в диапазоне P.root.

LaTeX

$$$ -P.root(i) \in \mathrm{range}(P.root) $$$

Lean4

theorem neg_root_mem : -P.root i ∈ range P.root :=
  ⟨P.reflectionPerm i i, by simp⟩

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

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

Разделы

Аффилиация

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