RootForm

Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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

English

The kernel of Polarization coincides with the kernel of RootForm: ker P.Polarization = ker P.RootForm.

Русский

Ядро отображения Polarization совпадает с ядром RootForm: ker P.Polarization = ker P.RootForm.

LaTeX

$$$ \\ker\\!P.Polarization = \\ker\\!P.RootForm $$$

Lean4

/-- An invariant inner product on the weight space. -/
def RootForm : LinearMap.BilinForm R M :=
  ∑ i, (P.coroot' i).smulRight (P.coroot' i)

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

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

Разделы

Аффилиация

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