English
Star is compatible with the canonical center-to-centroid map: star(centerToCentroidCenter z) = centerToCentroidCenter(star z).
Русский
Звезда совместима с каноническим отображением центра в центроид: звезда(centerToCentroidCenter z) = centerToCentroidCenter(star z).
LaTeX
$$$\\star(\\, centerToCentroidCenter(z)\\,) = centerToCentroidCenter(\\star z)$$$
Lean4
theorem star_centerToCentroidCenter (z : NonUnitalStarSubsemiring.center α) :
star (centerToCentroidCenter z) = (centerToCentroidCenter (star z : NonUnitalStarSubsemiring.center α)) :=
by
ext a
calc
(star (centerToCentroidCenter z)) a = star (z * star a) := rfl
_ = star (star a) * star z := by simp only [star_mul, star_star, StarMemClass.coe_star]
_ = a * star z := by rw [star_star]
_ = (star z) * a := by rw [(star z).property.comm]
_ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl
