coe_subtypeL — Mathlib

English

The inclusion of a submodule p into M1, viewed as a ContinuousLinearMap, coincides with the canonical lifting of p.subtype.

Русский

Включение подмодуля p в M1, рассматриваемое как непрерывно-линейное отображение, совпадает с каноническим встраиванием p.subtype.

LaTeX

$$$(p:\text{Submodule } R_1 M_1).subtypeL = p.subtypeL$ (as linear maps).$$

Lean4

@[simp, norm_cast]
theorem _root_.Submodule.coe_subtypeL (p : Submodule R₁ M₁) : (p.subtypeL : p →ₗ[R₁] M₁) = p.subtype :=
  rfl

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