threeShortAddLongRoot

Mathlib.LinearAlgebra.RootSystem.Finite.G2

URI: https://scilib.ai/kg/mathlib#RootPairing.EmbeddedG2.threeShortAddLongRoot

English

The root corresponding to 3α+β is threeShortAddLongRoot = P.root(threeShortAddLong P).

Русский

Корень, соответствующий 3α+β, задаётся как threeShortAddLongRoot = P.root(threeShortAddLong P).

LaTeX

$$$threeShortAddLongRoot = P.root(threeShortAddLong\ P)$$$

Lean4

/-- The short root `3α + β`. -/
abbrev threeShortAddLongRoot : M :=
  P.root (threeShortAddLong P)

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

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

Разделы

Аффилиация

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