instStar

Mathlib.Algebra.Star.CentroidHom

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

Lean4

instance : Star (CentroidHom α) where
  star
    f :=
    { toFun := fun a => star (f (star a))
      map_zero' := by simp only [star_zero, map_zero]
      map_add' := fun a b => by simp only [star_add, map_add]
      map_mul_left' := fun a b => by simp only [star_mul, map_mul_right, star_star]
      map_mul_right' := fun a b => by simp only [star_mul, map_mul_left, star_star] }

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

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

Разделы

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

Аффилиация

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