reflectionPerm_eq_iff_smul_coroot

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

Under suitable hypotheses (NeZero 2 and IsDomain), pairing i j = 0 iff pairing j i = 0.

Русский

При подходящих условиях (NeZero 2 и IsDomain) pairing i j = 0 эквивалентно pairing j i = 0.

LaTeX

$$$$ P.pairing(i,j) = 0 \\iff P.pairing(j,i) = 0. $$$$

Lean4

theorem reflectionPerm_eq_iff_smul_coroot : P.reflectionPerm i j = j ↔ P.pairing i j • P.coroot i = 0 :=
  P.flip.reflectionPerm_eq_iff_smul_root

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

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

Разделы

Аффилиация

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