domRestrict' — Mathlib

English

For a linear map f: M → M₂ and submodule p, the evaluation of domRestrict'(p) f at a point x ∈ p equals f(x).

Русский

Для линейного отображения f: M → M₂ и подпространства p значение (domRestrict' p f)(x) равно f(x) при x ∈ p.

LaTeX

$$$\\text{domRestrict}'(p)\\,f\\,x = f\\,x.$$$

Lean4

/-- Alternative version of `domRestrict` as a linear map. -/
def domRestrict' (p : Submodule R M) : (M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂
    where
  toFun φ := φ.domRestrict p
  map_add' := by simp [LinearMap.ext_iff]
  map_smul' := by simp [LinearMap.ext_iff]

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