instStarRing — Mathlib

English

The product R × S carries a star-ring structure with star acting componentwise: star((r,s)) = (star r, star s) and the ring operations are defined componentwise.

Русский

Произведение R × S имеет структуру звезда-кольца: star((r,s)) = (star r, star s) и операции кольца задаются по компонентам.

LaTeX

$$$\\\\star((r,s)) = (\\\\star r, \\\\star s).$$$

Lean4

instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [StarRing R] [StarRing S] : StarRing (R × S) :=
  { inferInstanceAs (StarAddMonoid (R × S)), inferInstanceAs (StarMul (R × S)) with }

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