coe_injective

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleHom.coe_injective

English

The underlying function map from LieModuleHom to functions is injective.

Русский

Взаимная биекция отображения из Ли-модуля в основанную функцию инъективна.

LaTeX

$$Injective( LieModuleHom.instFunLike.coe )$$

Lean4

theorem coe_injective : @Function.Injective (M →ₗ⁅R,L⁆ N) (M → N) (↑) :=
  by
  rintro ⟨⟨⟨f, _⟩⟩⟩ ⟨⟨⟨g, _⟩⟩⟩ h
  congr

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

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

Разделы

Аффилиация

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