isOrthogonal_symm

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

IsOrthogonal is symmetric: IsOrthogonal i j implies IsOrthogonal j i.

Русский

Свойство ортогональности симметрично: IsOrthogonal i j ⇒ IsOrthogonal j i.

LaTeX

$$$$ \\operatorname{IsOrthogonal}(P,i,j) \\iff \\operatorname{IsOrthogonal}(P,j,i). $$$$

Lean4

theorem isOrthogonal_symm : IsOrthogonal P i j ↔ IsOrthogonal P j i := by simp only [IsOrthogonal, and_comm]

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

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

Разделы

Аффилиация

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