Star on product types

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

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

Equations

• Prod.instStar = { star := fun (x : R × S) => (star x.1, star x.2) }

@[simp]

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

@[simp]

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

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

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

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

Equations

• Prod.instInvolutiveStar = { toStar := Prod.instStar, star_involutive := ⋯ }

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

Equations

• Prod.instStarMul = { toInvolutiveStar := Prod.instInvolutiveStar, star_mul := ⋯ }

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

Equations

• Prod.instStarAddMonoid = { toInvolutiveStar := Prod.instInvolutiveStar, star_add := ⋯ }

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

Equations

• Prod.instStarRing = { toInvolutiveStar := StarAddMonoid.toInvolutiveStar, star_mul := ⋯, star_add := ⋯ }

instance Prod.instStarModule {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ˣ) : (embedProduct R) (star u) = star ((embedProduct R) u)