neg_coroot_mem

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

If i, j ∈ ι and t ∈ R with P.root j = t · P.root i, then t · P.coroot j = P.coroot i.

Русский

Если j, i ∈ ι и P.root j = t · P.root i, то t · P.coroot j = P.coroot i.

LaTeX

$$$ P.root(j) = t \cdot P.root(i) \Rightarrow t \cdot P.coroot(j) = P.coroot(i) $$$

Lean4

theorem neg_coroot_mem : -P.coroot i ∈ range P.coroot :=
  P.flip.neg_root_mem i

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

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

Разделы

Аффилиация

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