# Documentation

Mathlib.Algebra.Star.Prod

# Star on product types #

We put a Star structure on product types that operates elementwise.

instance Prod.instStarProd {R : Type u} {S : Type v} [inst : Star R] [inst : Star S] :
Star (R × S)
Equations
• Prod.instStarProd = { star := fun x => (star x.fst, star x.snd) }
@[simp]
theorem Prod.fst_star {R : Type u} {S : Type v} [inst : Star R] [inst : Star S] (x : R × S) :
(star x).fst = star x.fst
@[simp]
theorem Prod.snd_star {R : Type u} {S : Type v} [inst : Star R] [inst : Star S] (x : R × S) :
(star x).snd = star x.snd
theorem Prod.star_def {R : Type u} {S : Type v} [inst : Star R] [inst : Star S] (x : R × S) :
star x = (star x.fst, star x.snd)
instance Prod.instInvolutiveStarProd {R : Type u} {S : Type v} [inst : ] [inst : ] :
Equations
instance Prod.instStarSemigroupProdInstSemigroupProd {R : Type u} {S : Type v} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance Prod.instStarAddMonoidProdInstAddMonoidSum {R : Type u} {S : Type v} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance Prod.instStarRingProdInstNonUnitalSemiringProd {R : Type u} {S : Type v} [inst : ] [inst : ] [inst : ] [inst : ] :
StarRing (R × S)
Equations
• One or more equations did not get rendered due to their size.
instance Prod.instStarModuleProdInstStarProdSmul {R : Type u} {S : Type v} {α : Type w} [inst : SMul α R] [inst : SMul α S] [inst : Star α] [inst : Star R] [inst : Star S] [inst : ] [inst : ] :
StarModule α (R × S)
Equations
theorem Units.embed_product_star {R : Type u} [inst : ] [inst : ] (u : Rˣ) :
↑() (star u) = star (↑() u)