instCentroidHomClass — Mathlib

English

There is a canonical CentroidHomClass structure on CentroidHom α with the usual map properties (zero, addition, left and right multiplication).

Русский

Существует каноническая структура CentroidHomClass на CentroidHom α, задающая обычные свойства отображения ( нуль, сложение, умножение слева и справа ).

LaTeX

$$$\\operatorname{CentroidHomClass}(\\operatorname{CentroidHom} \\alpha, \\alpha)$$$

Lean4

instance : CentroidHomClass (CentroidHom α) α
    where
  map_zero f := f.map_zero'
  map_add f := f.map_add'
  map_mul_left f := f.map_mul_left'
  map_mul_right f := f.map_mul_right'

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