toMonoidWithZeroHom

Mathlib.Algebra.GroupWithZero.Hom

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHomClass.toMonoidWithZeroHom

Lean4

/-- Turn an element of a type `F` satisfying `MonoidWithZeroHomClass F α β` into an actual
`MonoidWithZeroHom`. This is declared as the default coercion from `F` to `α →*₀ β`. -/
@[coe]
def toMonoidWithZeroHom [FunLike F α β] [MonoidWithZeroHomClass F α β] (f : F) : α →*₀ β :=
  { (f : α →* β), (f : ZeroHom α β) with }

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

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

Разделы

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

Аффилиация

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