domRestrict₂ — Mathlib

English

For any bilinear map f, f(x, y1+y2) = f(x, y1) + f(x, y2).

Русский

Для билинейного отображения f: f(x, y1+y2) = f(x, y1) + f(x, y2).

LaTeX

$$$ f(x, y_1 + y_2) = f(x, y_1) + f(x, y_2) $$$

Lean4

/-- Restricting a bilinear map in the second entry -/
def domRestrict₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) : M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P
    where
  toFun m := (f m).domRestrict q
  map_add' m₁ m₂ := LinearMap.ext fun _ => by simp only [map_add, domRestrict_apply, add_apply]
  map_smul' c m := LinearMap.ext fun _ => by simp only [f.map_smulₛₗ, domRestrict_apply, smul_apply]

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