restrictScalars₁₂ — Mathlib

English

If f is bilinear, then its restricted form satisfies (f.domRestrict₁₂ p q) x y = f x y for x ∈ p, y ∈ q.

Русский

Если f билинейна, то её ограниченная форма удовлетворяет (f.domRestrict₁₂ p q) x y = f x y для x ∈ p, y ∈ q.

LaTeX

$$$ (f.domRestrict₁₂ p q) x y = f x y $$$

Lean4

/-- If `B : M → N → Pₗ` is `R`-`S` bilinear and `R'` and `S'` are compatible scalar multiplications,
then the restriction of scalars is a `R'`-`S'` bilinear map. -/
@[simps!]
def restrictScalars₁₂ (B : M →ₗ[R] N →ₗ[S] Pₗ) : M →ₗ[R'] N →ₗ[S'] Pₗ :=
  LinearMap.mk₂' R' S' (B · ·) B.map_add₂
    (fun r' m _ ↦ by
      dsimp only
      rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul])
    (fun _ ↦ map_add _) (fun _ x ↦ (B x).map_smul_of_tower _)

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