instStarAddMonoidCenter — Mathlib

English

The center of CentroidHom α forms a StarAddMonoid under the induced pointwise operations.

Русский

Центр CentroidHom α образует звездно-аддитивный моноид под индуцированными покомпонентными операциями.

LaTeX

$$$\\forall f,g\\in\\mathrm{Subsemiring.center}(\\mathrm{CentroidHom}(\\alpha)),\\star(f+g)=\\star f+\\star g,\\; \\star(\\star f)=f$$$

Lean4

instance instStarAddMonoidCenter : StarAddMonoid (Subsemiring.center (CentroidHom α))
    where
  star_involutive f := SetCoe.ext (star_involutive f.val)
  star_add f g := SetCoe.ext (star_add f.val g.val)

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