restrictScalarsField_apply_apply — Mathlib

English

Restricting scalars for a perfect pairing yields a new perfect pairing on the restricted modules with the same bilinear form structure.

Русский

Ограничение скаляров для совершенного парирования образует новое совершенное парирование на ограниченных модулях с той же билинейной структурой.

LaTeX

$$PerfectPairing.restrictScalars : PerfectPairing$$

Lean4

@[simp]
theorem restrictScalarsField_apply_apply (hp : ∀ m n, p (i m) (j n) ∈ (algebraMap K L).range) (x : M') (y : N') :
    algebraMap K L
        (LinearMap.restrictScalarsRange₂ i j (Algebra.linearMap K L) (FaithfulSMul.algebraMap_injective K L) p hp x y) =
      p (i x) (j y) :=
  LinearMap.restrictScalarsRange₂_apply i j (Algebra.linearMap K L) (FaithfulSMul.algebraMap_injective K L) p hp x y

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