twoShortAddLongRoot

Mathlib.LinearAlgebra.RootSystem.Finite.G2

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

English

The root corresponding to 2α+β is given by twoShortAddLongRoot = P.root(twoShortAddLong P).

Русский

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

LaTeX

$$$twoShortAddLongRoot = P.root(twoShortAddLong\ P)$$$

Lean4

/-- The short root `2α + β`. -/
abbrev twoShortAddLongRoot : M :=
  P.root (twoShortAddLong P)

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

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

Разделы

Аффилиация

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