hasCoeToLieModuleHom

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleEquiv.hasCoeToLieModuleHom

English

There is a natural coercion from LieModuleEquiv to LieModuleHom given by the underlying map.

Русский

Существует естественное приведение из LieModuleEquiv в LieModuleHom по основанной карте.

LaTeX

$$$e \mapsto e.toLieModuleHom$$$

Lean4

instance hasCoeToLieModuleHom : Coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N) :=
  ⟨toLieModuleHom⟩

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

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

Разделы

Аффилиация

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