comp

Mathlib.Algebra.Ring.CentroidHom

URI: https://scilib.ai/kg/mathlib#CentroidHom.comp

Lean4

/-- Composition of `CentroidHom`s as a `CentroidHom`. -/
def comp (g f : CentroidHom α) : CentroidHom α :=
  {
    g.toAddMonoidHom.comp
      f.toAddMonoidHom with
    map_mul_left' := fun _a _b ↦ (congr_arg g <| f.map_mul_left' _ _).trans <| g.map_mul_left' _ _
    map_mul_right' := fun _a _b ↦ (congr_arg g <| f.map_mul_right' _ _).trans <| g.map_mul_right' _ _ }

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

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

Разделы

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

Аффилиация

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