toMonoidHom

Mathlib.Algebra.Group.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#MulEquiv.toMonoidHom

Lean4

/-- Extract the forward direction of a multiplicative equivalence
as a multiplication-preserving function.
-/
@[to_additive /-- Extract the forward direction of an additive equivalence
      as an addition-preserving function. -/
    ]
def toMonoidHom (h : M ≃* N) : M →* N :=
  { h with map_one' := h.map_one }

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

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

Разделы

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

Аффилиация

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