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)

Equations

• Prod.instStarProd = { star := fun x => (star x.fst, star x.snd) }

@[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)

Equations

• @Prod.instTrivialStarProdInstStarProd = @Prod.instTrivialStarProdInstStarProd.proof_1

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

Equations

• Prod.instInvolutiveStarProd = InvolutiveStar.mk (_ : ∀ (x : R × S), star (star x) = x)

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

Equations

• Prod.instStarMulProdInstMul = StarMul.mk (_ : ∀ (x x_1 : R × S), star (x * x_1) = star x_1 * star x)

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

Equations

• Prod.instStarAddMonoidProdInstAddMonoid = StarAddMonoid.mk (_ : ∀ (x x_1 : R × S), star (x + x_1) = star x + star x_1)

instance Prod.instStarRingProdInstNonUnitalNonAssocSemiring {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [StarRing R] [StarRing S] : 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} [SMul α R] [SMul α S] [Star α] [Star R] [Star S] [StarModule α R] [StarModule α S] : StarModule α (R × S)

Equations

• @Prod.instStarModuleProdInstStarProdSmul = @Prod.instStarModuleProdInstStarProdSmul.proof_1

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