threeShortAddTwoLongRoot

Mathlib.LinearAlgebra.RootSystem.Finite.G2

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

English

The root corresponding to 3α+2β is threeShortAddTwoLongRoot = P.root(threeShortAddTwoLong P).

Русский

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

LaTeX

$$$threeShortAddTwoLongRoot = P.root(threeShortAddTwoLong\ P)$$$

Lean4

/-- The short root `3α + 2β`. -/
abbrev threeShortAddTwoLongRoot : M :=
  P.root (threeShortAddTwoLong P)

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

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

Разделы

Аффилиация

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