instStarMul — Mathlib

English

The star operation on the product respects multiplication: star((r1,s1)·(r2,s2)) = star(r1,r2) · star(s1,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) \\\\cdot (r_2,s_2)) = (\\\\star r_1 \\\\cdot \\\\star r_2, \\\\star s_1 \\\\cdot \\\\star s_2).$$$

Lean4

instance [Mul R] [Mul S] [StarMul R] [StarMul S] : StarMul (R × S) where
  star_mul _ _ := Prod.ext (star_mul _ _) (star_mul _ _)

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