English
If P.root k = x • P.root i + y • P.root l, then P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j for all j.
Русский
Если P.root k равно x • P.root i + y • P.root l, тогда P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j.
LaTeX
$$$P.root\;k = x \cdot P.root\;i + y \cdot P.root\;l \Rightarrow P.pairingIn\;S\;k\;j = x \cdot P.pairingIn\;S\;i\;j + y \cdot P.pairingIn\;S\;l\;j$$$
Lean4
theorem pairingIn_eq_add_of_root_eq_smul_add_smul [FaithfulSMul S R] [P.IsValuedIn S] [Module S M] [IsScalarTower S R M]
{i j k l : ι} {x y : S} (h : P.root k = x • P.root i + y • P.root l) :
P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j :=
by
apply FaithfulSMul.algebraMap_injective S R
replace h : P.root k = (algebraMap S R x) • P.root i + (algebraMap S R y) • P.root l := by simpa
simpa [← P.algebraMap_pairingIn S, -algebraMap_pairingIn] using pairing_eq_add_of_root_eq_smul_add_smul h
