ofSubmodule'_toLinearMap — Mathlib

English

A variant of restricting a linear equivalence to the preimage of a submodule (left-side restriction).

Русский

Вариант ограничения линейного эквивалента к прообразу подмодуля (левое ограничение).

LaTeX

$$def ofSubmodule' (f) (U) : U.comap f ≃_l[R] U$$

Lean4

theorem ofSubmodule'_toLinearMap [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
    (f.ofSubmodule' U).toLinearMap = (f.toLinearMap.domRestrict _).codRestrict _ Subtype.prop :=
  by
  ext
  rfl

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