long_eq_three_mul_short — Mathlib

English

The invariant form scales the self-pairing of the long root by three times the self-pairing of the short root: B.form(longRoot, longRoot) = 3 B.form(shortRoot, shortRoot).

Русский

Самопропорция длинного корня равна тройному самопримыканию короткого корня: B(longRoot, longRoot) = 3 B(shortRoot, shortRoot).

LaTeX

$$$B\text{.form}(\text{longRoot}(P),\text{longRoot}(P)) = 3 \cdot B\text{.form}(\text{shortRoot}(P),\text{shortRoot}(P))$$$

Lean4

theorem long_eq_three_mul_short : B.form (longRoot P) (longRoot P) = 3 * B.form (shortRoot P) (shortRoot P) := by
  simpa using B.pairing_mul_eq_pairing_mul_swap (long P) (short P)

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