pairing_mul_eq_pairing_mul_swap — Mathlib

English

The product of pairings with swapped indices matches: P.pairing j i · B.form (P.root i) (P.root i) equals P.pairing i j · B.form (P.root j) (P.root j).

Русский

Произведение парирований с поменянными индексами совпадает: pairing j i · B.form (P.root i) (P.root i) = pairing i j · B.form (P.root j) (P.root j).

LaTeX

$$$ P.pairing\\ j\\ i \\cdot B.form\\bigl(P.root\\ i\\bigr)\\bigl(P.root\\ i\\bigr) = P.pairing\\ i\\ j \\cdot B.form\\bigl(P.root\\ j\\bigr)\\bigl(P.root\\ j\\bigr) $$$

Lean4

theorem pairing_mul_eq_pairing_mul_swap :
    P.pairing j i * B.form (P.root i) (P.root i) = P.pairing i j * B.form (P.root j) (P.root j) := by
  rw [← B.two_mul_apply_root_root i j, ← B.two_mul_apply_root_root j i, ← B.symm.eq, RingHom.id_apply]

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