coroot_eq_neg_iff

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

If P.root i = t · P.root j for some t ∈ R, then P.coroot i = t · P.coroot j.

Русский

Если корень i равен t · корень j, то короот i равен t · короот j.

LaTeX

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

Lean4

@[simp]
theorem coroot_eq_neg_iff : P.coroot i = -P.coroot j ↔ i = P.reflectionPerm j j :=
  P.flip.root_eq_neg_iff

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

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

Разделы

Аффилиация

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