instStarRingSubtypeMemSubsemiringCenter

English

The center, as a subtype, becomes a StarRing with the star-compatibility condition star(fg) = star g · star f.

Русский

Центр в виде подтипа образует звездо-кольцо, удовлетворяющее совместимости со звездой: звезда от произведения равна произведению звезд в обратном порядке.

LaTeX

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

Lean4

instance : StarRing (Subsemiring.center (CentroidHom α))
    where
  __ := instStarAddMonoidCenter
  star_mul f
    g := by
    ext a
    calc
      star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
      _ = star (g (f (star a))) := rfl
      _ = star (g (star (star (f (star a))))) := by simp only [star_star]
      _ = (star g * star f) a := rfl

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