coe_toSubmodule

Mathlib.Algebra.Lie.Submodule

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

English

The equality (N.toSubmodule) equals the canonical Submodule underlying N; i.e., the carrier is exactly the Submodule.

Русский

Равенство (N.toSubmodule) = N как подмодуль: носитель равен подмодулю.

LaTeX

$$$(N.toSubmodule) = N$ as Submodule/R-M terms$$

Lean4

@[norm_cast]
theorem coe_toSubmodule : ((N : Submodule R M) : Set M) = N :=
  rfl

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

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

Разделы

Аффилиация

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