twoShortAddLongRoot_eq

Mathlib.LinearAlgebra.RootSystem.Finite.G2

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

← MathLib Explorer

English

ThreeShortAddLongRoot equals 3 times shortRoot plus one longRoot: threeShortAddLongRoot = 3·shortRoot + longRoot.

Русский

ThreeShortAddLongRoot равно 3·shortRoot + longRoot.

LaTeX

$$$threeShortAddLongRoot = 3\,shortRoot + longRoot$$$

Lean4

theorem twoShortAddLongRoot_eq : twoShortAddLongRoot P = (2 : R) • shortRoot P + longRoot P :=
  by
  simp [twoShortAddLongRoot, twoShortAddLong, reflection_apply_root]
  module

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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