reflectionPerm_eq_of_pairing_eq_zero

Mathlib.LinearAlgebra.RootSystem.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem reflectionPerm_eq_of_pairing_eq_zero (h : P.pairing j i = 0) : P.reflectionPerm i j = j :=
  P.root.injective <| by simp [reflection_apply, h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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