instTrivialStar — Mathlib

English

If R and S have trivial star operations, then the product R × S carries a canonical componentwise star operation; in particular star(r,s) = (star r, star s).

Русский

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

LaTeX

$$$\\\\forall (r,s) \\\\in R \\times S, \\\\ star(r,s) = (star(r), star(s)).$$$

Lean4

instance [Star R] [Star S] [TrivialStar R] [TrivialStar S] : TrivialStar (R × S) where
  star_trivial _ := Prod.ext (star_trivial _) (star_trivial _)

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