ofSubmodule'_apply — Mathlib

English

The map part of the left-restricted equivalence coincides with the expected codomain restriction.

Русский

Часть отображения левого ограничения совпадает с ожидаемым ограничением кодом.

LaTeX

$$theorem ofSubmodule'_toLinearMap (f) (U) : (f.ofSubmodule' U).toLinearMap = (f.toLinearMap.domRestrict _).codRestrict _ Subtype.prop$$

Lean4

@[simp]
theorem ofSubmodule'_apply [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂)
    (x : U.comap (f : M →ₛₗ[σ₁₂] M₂)) : (f.ofSubmodule' U x : M₂) = f (x : M) :=
  rfl

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