instance
Prod.instInvolutiveStarProd
{R : Type u}
{S : Type v}
[inst : InvolutiveStar R]
[inst : InvolutiveStar S]
:
InvolutiveStar (R × S)
instance
Prod.instStarSemigroupProdInstSemigroupProd
{R : Type u}
{S : Type v}
[inst : Semigroup R]
[inst : Semigroup S]
[inst : StarSemigroup R]
[inst : StarSemigroup S]
:
StarSemigroup (R × S)
instance
Prod.instStarAddMonoidProdInstAddMonoidSum
{R : Type u}
{S : Type v}
[inst : AddMonoid R]
[inst : AddMonoid S]
[inst : StarAddMonoid R]
[inst : StarAddMonoid S]
:
StarAddMonoid (R × S)
instance
Prod.instStarRingProdInstNonUnitalSemiringProd
{R : Type u}
{S : Type v}
[inst : NonUnitalSemiring R]
[inst : NonUnitalSemiring S]
[inst : StarRing R]
[inst : StarRing 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 : StarModule α R]
[inst : StarModule α S]
:
StarModule α (R × S)
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)