English
The theorem provides that star-structure on Subsemiring.center(CentroidHom α) respects multiplication: star(f g) = star g · star f.
Русский
Теорема устанавливает, что звездная структура Subsemiring.center(CentroidHom α) совместима с умножением: star(f g) = star g star f.
LaTeX
$$$\\forall f,g \\in \\mathrm{Subsemiring.center}(\\mathrm{CentroidHom}(\\alpha)),\\quad \\star(fg)=\\star g\\;\\star f$$$
Lean4
/-- The canonical *-homomorphism from the center of a non-unital, non-associative *-semiring into
the center of its centroid. -/
def starCenterToCentroidCenter : NonUnitalStarSubsemiring.center α →⋆ₙ+* Subsemiring.center (CentroidHom α)
where
toNonUnitalRingHom := centerToCentroidCenter
map_star'
_ := by
simp only [MulHom.toFun_eq_coe, NonUnitalRingHom.coe_toMulHom]
exact (star_centerToCentroidCenter _).symm
