coeFn

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#MulHom.coeFn

Lean4

/-- Coercion of a `MulHom` into a function is itself a `MulHom`.

See also `MulHom.eval`. -/
@[to_additive (attr := simps) /-- Coercion of an `AddHom` into a function is itself an `AddHom`.

    See also `AddHom.eval`. -/
    ]
def coeFn (α β : Type*) [Mul α] [CommSemigroup β] : (α →ₙ* β) →ₙ* α → β
    where
  toFun g := g
  map_mul' _ _ := rfl

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

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

Разделы

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

Аффилиация

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