incl_coe

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.incl_coe

English

The inclusion map coincides with the inclusion into the ambient submodule's subtype.

Русский

Включение совпадает с вложением в подмодуль как подтип.

LaTeX

$$inclusion_coe : (N.incl) = (N : Submodule R M).subtype$$

Lean4

@[simp]
theorem incl_coe : (N.incl : N →ₗ[R] M) = (N : Submodule R M).subtype :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru