instMul

Mathlib.Algebra.Group.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OneHom.instMul

Lean4

/-- Given two one-preserving morphisms `f`, `g`,
`f * g` is the one-preserving morphism sending `x` to `f x * g x`. -/
@[to_additive /-- Given two zero-preserving morphisms `f`, `g`,
    `f + g` is the zero-preserving morphism sending `x` to `f x + g x`. -/
    ]
instance [One M] [MulOneClass N] : Mul (OneHom M N) where
  mul f
    g :=
    { toFun m := f m * g m
      map_one' := by simp }

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

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

Разделы

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

Аффилиация

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