instStarAddMonoid — Mathlib

English

The star operation on the product respects addition: star((r1,s1)+(r2,s2)) = (star r1 + star r2, star s1 + star s2).

Русский

Операция звезды на произведении сохраняет сложение: star((r1,s1)+(r2,s2)) = (star r1 + star r2, star s1 + star s2).

LaTeX

$$$\\\\star((r_1,s_1) + (r_2,s_2)) = (\\\\star r_1 + \\\\star r_2, \\\\star s_1 + \\\\star s_2).$$$

Lean4

instance [AddMonoid R] [AddMonoid S] [StarAddMonoid R] [StarAddMonoid S] : StarAddMonoid (R × S) where
  star_add _ _ := Prod.ext (star_add _ _) (star_add _ _)

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