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 _)