instStarSubtypeMemSubsemiringCenter

English

The center of CentroidHom α (as a subsemiring) inherits a star-add-monoid structure.

Русский

Центр CentroidHom α (как подполином) наследует структуру звездного аддитивного моноида.

LaTeX

$$$\\text{StarAddMonoid}(\\mathrm{Subsemiring.center}(\\mathrm{CentroidHom}(\\alpha)))$ with pointwise operations$$

Lean4

instance : Star (Subsemiring.center (CentroidHom α)) where
  star
    f :=
    ⟨star (f : CentroidHom α),
      Subsemiring.mem_center_iff.mpr
        (fun g =>
          ext
            (fun a =>
              calc
                g (star (f (star a))) = star (star g (f (star a))) := by rw [star_apply, star_star]
                _ = star ((star g * f) (star a)) := rfl
                _ = star ((f * star g) (star a)) := by rw [f.property.comm]
                _ = star (f (star g (star a))) := rfl
                _ = star (f (star (g a))) := by rw [star_apply, star_star]))⟩

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