English
Let P be a RootPairing with appropriate scalar structures. Then the pairings satisfy: if P.pairingIn S i j = 1 and P.pairingIn S j i = 4, then P.root j = 2 · P.root i, and conversely.
Русский
Пусть 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_one_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_one_four_iff, ← P.algebraMap_pairingIn S, ← P.algebraMap_pairingIn S, ← map_one (algebraMap S R), ←
map_ofNat (algebraMap S R), (algebraMap_injective S R).eq_iff, (algebraMap_injective S R).eq_iff]
