English
For each i, the star of the i-th coordinate in the singleton is the singleton of the star of that coordinate: Pi.single i (star a) = star (Pi.single i a).
Русский
Для каждого i звезда в i-й координате единичного набора равна единичному набору после применения звезды к координате: Pi.single i (star a) = star (Pi.single i a).
LaTeX
$$$\\mathrm{Pi.single}_i(\\star a) = \\star\\big(\\mathrm{Pi.single}_i a\\big).$$$
Lean4
theorem single_star [∀ i, AddMonoid (f i)] [∀ i, StarAddMonoid (f i)] [DecidableEq I] (i : I) (a : f i) :
Pi.single i (star a) = star (Pi.single i a) :=
single_op (fun i => @star (f i) _) (fun _ => star_zero _) i a
