toLinearPMap — Mathlib

English

On an element x in the projecting submodule, g.toLinearPMap x equals valFromGraph hg x.2.

Русский

На элементе x из проекции графа g.toLinearPMap x равно valFromGraph hg x.2.

LaTeX

$$g.toLinearPMap x = valFromGraph hg x.2$$

Lean4

/-- Define a `LinearPMap` from its graph.

In the case that the submodule is not a graph of a `LinearPMap` then the underlying linear map
is just the zero map. -/
noncomputable def toLinearPMap (g : Submodule R (E × F)) : E →ₗ.[R] F
    where
  domain := g.map (LinearMap.fst R E F)
  toFun := if hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0 then g.toLinearPMapAux hg else 0

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