Star on product types

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

instance Prod.instStarProd {R : Type u} {S : Type v} [Star R] [Star S] : Star (R × S)

@[simp]

theorem Prod.fst_star {R : Type u} {S : Type v} [Star R] [Star S] (x : R × S) : (star x).fst = star x.fst

@[simp]

theorem Prod.snd_star {R : Type u} {S : Type v} [Star R] [Star S] (x : R × S) : (star x).snd = star x.snd

theorem Prod.star_def {R : Type u} {S : Type v} [Star R] [Star S] (x : R × S) : star x = (star x.fst, star x.snd)

instance Prod.instTrivialStarProdInstStarProd {R : Type u} {S : Type v} [Star R] [Star S] [TrivialStar R] [TrivialStar S] : TrivialStar (R × S)

instance Prod.instInvolutiveStarProd {R : Type u} {S : Type v} [InvolutiveStar R] [InvolutiveStar S] : InvolutiveStar (R × S)

instance Prod.instStarMulProdInstMul {R : Type u} {S : Type v} [Mul R] [Mul S] [StarMul R] [StarMul S] : StarMul (R × S)

instance Prod.instStarAddMonoidProdInstAddMonoid {R : Type u} {S : Type v} [AddMonoid R] [AddMonoid S] [StarAddMonoid R] [StarAddMonoid S] : StarAddMonoid (R × S)

instance Prod.instStarRingProdInstNonUnitalNonAssocSemiring {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [StarRing R] [StarRing S] : StarRing (R × S)

instance Prod.instStarModuleProdInstStarProdSmul {R : Type u} {S : Type v} {α : Type w} [SMul α R] [SMul α S] [Star α] [Star R] [Star S] [StarModule α R] [StarModule α S] : StarModule α (R × S)

theorem Units.embed_product_star {R : Type u} [Monoid R] [StarMul R] (u : Rˣ) : ↑(Units.embedProduct R) (star u) = star (↑(Units.embedProduct R) u)