restrictScalars_pairing — Mathlib

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]

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