threeShortAddLongRoot_longRoot — Mathlib

English

For an invariant form B associated to a RootPairing EmbeddedG2, the evaluation on the root threeShortAddLongRoot(P) with itself equals the evaluation on longRoot(P) with itself.

Русский

Для инвариантной формы B, связанной с корневым парингом EmbeddedG2, значение B на корне threeShortAddLongRoot(P) в паре с самим собой равно значению B на корне longRoot(P) в паре с самим собой.

LaTeX

$$$ B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) = B.form (longRoot P) (longRoot P) $$$

Lean4

/-- `3α + β` is long. -/
@[simp]
theorem threeShortAddLongRoot_longRoot :
    B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) = B.form (longRoot P) (longRoot P) := by
  simp [threeShortAddLongRoot, threeShortAddLong]

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