coroot_root_two

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The reflection associated to a root is a linear automorphism of M.

Русский

Связанная с корнем отражение является линейной автоматикой пространства M.

LaTeX

$$$ \mathrm{reflection} : M \to M \quad \text{is a linear isomorphism} $$$

Lean4

theorem coroot_root_two : P.toLinearMap.flip (P.coroot i) (P.root i) = 2 := by simp

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

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

Разделы

Аффилиация

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