instModuleHom

Mathlib.Algebra.Homology.ShortComplex.Linear

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.instModuleHom

← MathLib Explorer

English

For any S1, S2, the set Hom(S1,S2) is a module over R.

Русский

Для любых S1, S2 множество Hom(S1,S2) является модулем над R.

LaTeX

$$$\mathrm{Module}_R(\mathrm{Hom}(S_1,S_2))$$$

Lean4

instance : Module R (S₁ ⟶ S₂) where
  zero_smul := by cat_disch
  one_smul := by cat_disch
  smul_zero := by cat_disch
  smul_add := by cat_disch
  add_smul := by cat_disch
  mul_smul := by cat_disch

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

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

Разделы

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

Аффилиация

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