toLinearMap_injective

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#DistribMulActionHom.toLinearMap_injective

← MathLib Explorer

English

The map from DistribMulActionHom to LinearMap is injective.

Русский

Отображение DistribMulActionHom в LinearMap инъективно.

LaTeX

$$$\text{toLinearMap_injective}$: injective mapping from DistribMulActionHom to LinearMap.$$

Lean4

theorem toLinearMap_injective {f g : M →ₑ+[σ.toMonoidHom] M₂} (h : (f : M →ₛₗ[σ] M₂) = (g : M →ₛₗ[σ] M₂)) : f = g :=
  by
  ext m
  exact LinearMap.congr_fun h m

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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