pairingIn_neg_one_neg_four_iff — Mathlib

English

Let P be a RootPairing as above. Then P.pairingIn S i j = -1 and P.pairingIn S j i = -4 if and only if P.root j = (-2) · P.root i.

Русский

Пусть P — парирование корней. Тогда P.pairingIn S i j = -1 и P.pairingIn S j i = -4 эквивалентно P.root j = (-2) · P.root i.

LaTeX

$$$ P.pairingIn\\ S\\ i\\ j = -1 \\land P.pairingIn\\ S\\ j\\ i = -4 \iff P.root\\ j = (-2) \\cdot P.root\\ i $$$

Lean4

theorem pairingIn_neg_one_neg_four_iff [IsDomain R] :
    P.pairingIn S i j = -1 ∧ P.pairingIn S j i = -4 ↔ P.root j = (-2 : R) • P.root i := by
  rw [← P.pairing_neg_one_neg_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S, ←
    map_one (algebraMap S R), ← map_ofNat (algebraMap S R), ← map_neg, ← map_neg, (algebraMap_injective S R).eq_iff,
    (algebraMap_injective S R).eq_iff]

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