English
Restriction of scalars intertwines the pairings: for all i, j, the base-map algebra sends the restricted pairing to the original pairing.
Русский
Ограничение скаляров сохраняет пары: для всех i, j алгебра-образ ограниченного спаривания даёт исходное спаривание.
LaTeX
$$$\\forall i,j:\\ algebraMap K L\\bigl( (P.restrictScalars' K hP).pairing(i,j) \\bigr) = P.pairing(i,j)$$$
Lean4
@[simp]
theorem restrictScalars_pairing (i j : ι) : algebraMap K L ((P.restrictScalars' K hP).pairing i j) = P.pairing i j := by
simp only [pairing, restrictScalars_toLinearMap_apply_apply, restrictScalars_coe_root, restrictScalars_coe_coroot]