instInvolutiveStar — Mathlib

English

If R and S carry involutive stars, then the product R × S inherits an involutive star given componentwise: star(star(r,s)) = (r,s).

Русский

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

LaTeX

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

Lean4

instance [InvolutiveStar R] [InvolutiveStar S] : InvolutiveStar (R × S) where
  star_involutive _ := Prod.ext (star_star _) (star_star _)

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