hom_zsmul

Mathlib.Algebra.Category.Grp.Preadditive

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.hom_zsmul

English

For natural n, the smul on morphisms commutes with taking the underlying hom.

Русский

Для натурального n умножение сохраняется на уровне гомоморфизмов и их подстановки.

LaTeX

$$$\\mathrm{Hom}(n \\cdot f) = n \\cdot \\mathrm{Hom}(f)$$$

Lean4

@[simp]
theorem hom_zsmul (n : ℕ) (f : M ⟶ N) : (n • f).hom = n • f.hom :=
  rfl

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

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

Разделы

Аффилиация

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