domRestrict₁₂_apply — Mathlib

English

Restricting a bilinear map in both arguments yields a bilinear map on paired substructures, i.e. p and q.

Русский

Ограничение билинейной карты по обеим аргументациям даёт билинейную карту на пары подструктур.

LaTeX

$$$ (f.domRestrict₁₂ p q) : p →ₗ[ρ_1^2] q →ₗ[σ_1^2] P $$$

Lean4

theorem domRestrict₁₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) (x : p) (y : q) :
    f.domRestrict₁₂ p q x y = f x y :=
  rfl

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