algebraMap_pairingIn — Mathlib

English

For a valued RootPairing P and indices i, j, the value of pairingIn, when mapped to R via the base algebra, coincides with the standard pairing: algebraMap S R (P.pairingIn S i j) = P.pairing i j.

Русский

Для ценованного корневого парирования P и индексов i, j, значение pairingIn переводится в R так, что algebraMap S R (P.pairingIn S i j) = P.pairing i j.

LaTeX

$$$\operatorname{algebraMap}_{S\to R}(P.pairingIn\;S\;i\;j) = P.pairing\;i\;j$$$

Lean4

@[simp]
theorem algebraMap_pairingIn [P.IsValuedIn S] (i j : ι) : algebraMap S R (P.pairingIn S i j) = P.pairing i j :=
  (P.exists_value i j).choose_spec

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