instStar — Mathlib

English

If R and S are equipped with an involution *, then the product R × S is equipped with the involution defined componentwise by star(r,s) = (star r, star s).

Русский

Если формы R и S имеют операцию сопряжения *, то произведение R × S имеет сопряжение, заданное по координатам: star(r,s) = (star r, star s).

LaTeX

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

Lean4

instance : Star (R × S) where star x := (star x.1, star x.2)

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