reflectionPerm_eq_of_pairing_eq_zero'

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.reflectionPerm_eq_of_pairing_eq_zero'

English

If pairing i j = 0, then reflectionPerm i j = j.

Русский

Если pairing i j = 0, то reflectionPerm i j = j.

LaTeX

$$$$ P.reflectionPerm(i,j) = j $$$$

Lean4

theorem reflectionPerm_eq_of_pairing_eq_zero' (h : P.pairing i j = 0) : P.reflectionPerm i j = j :=
  P.flip.reflectionPerm_eq_of_pairing_eq_zero h

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

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

Разделы

Аффилиация

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