domRestrict — Mathlib

English

As above, the sum of images equals the image of the sum under the inclusion.

Русский

Как выше, сумма изображений равна изображению суммы под включением.

LaTeX

$$$\uparrow(\sum_i x_i) = \sum_i \uparrow x_i$$$

Lean4

/-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map
`p → M₂`. -/
def domRestrict (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) : p →ₛₗ[σ₁₂] M₂ :=
  f.comp p.subtype

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