Star on product types

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

ink

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) }

ink

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

ink

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

ink

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)

ink

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

Equations

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

ink

instance Prod.instStarSemigroupProdInstSemigroupProd {R : Type u} {S : Type v} [inst : Semigroup R] [inst : Semigroup S] [inst : StarSemigroup R] [inst : StarSemigroup S] : StarSemigroup (R × S)

Equations

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

ink

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

Equations

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

ink

instance Prod.instStarRingProdInstNonUnitalSemiringProd {R : Type u} {S : Type v} [inst : NonUnitalSemiring R] [inst : NonUnitalSemiring S] [inst : StarRing R] [inst : StarRing S] : StarRing (R × S)

Equations

• One or more equations did not get rendered due to their size.

ink

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 : StarModule α R] [inst : StarModule α S] : StarModule α (R × S)

Equations

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

ink

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