identityMapOfZeroModuleIsZero

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.identityMapOfZeroModuleIsZero

← MathLib Explorer

English

The negation of a linear map composed with another equals the composition with the negated map: (−g) ∘ f = −(g ∘ f).

Русский

Отрицание композиции: (−g) ∘ f = −(g ∘ f).

LaTeX

$$(-g).comp f = - (g.comp f)$$

Lean4

/-- If `M` is the zero module, then the identity map of `M` is the zero map. -/
@[simp]
theorem identityMapOfZeroModuleIsZero [Subsingleton M] : id (R := R₁) (M := M) = 0 :=
  Subsingleton.eq_zero id

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

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

Разделы

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

Аффилиация

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