instDiv

Mathlib.Algebra.Group.Hom.Basic

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

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 additive morphism sending `x` to `f x - g x`. -/
    ]
instance [One M] [DivisionMonoid N] : Div (OneHom M N) where
  div f
    g :=
    { toFun m := f m / g m
      map_one' := by simp }

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

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

Разделы

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

Аффилиация

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