two_mul_apply_root_root — Mathlib

English

From the two-mul relation, one derives P.pairingIn S j i · B.rootLength i = P.pairingIn S i j · B.rootLength j.

Русский

Из двухумножения следует равенство: pairingIn S j i · B.rootLength i = pairingIn S i j · B.rootLength j.

LaTeX

$$$ P.pairingIn\\ S\\ j\\ i \\cdot B.rootLength i = P.pairingIn\\ S\\ i\\ j \\cdot B.rootLength j $$$

Lean4

theorem two_mul_apply_root_root : 2 * B.form (P.root i) (P.root j) = P.pairing i j * B.form (P.root j) (P.root j) :=
  B.toInvariantForm.two_mul_apply_root_root i j

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