Basic Results about Star on Product Type #
This file provides basic results about the star on product types defined in
Mathlib/Algebra/Notation/Prod.lean.
instance
Prod.instTrivialStar
{R : Type u}
{S : Type v}
[Star R]
[Star S]
[TrivialStar R]
[TrivialStar S]
:
TrivialStar (R × S)
@[implicit_reducible]
instance
Prod.instInvolutiveStar
{R : Type u}
{S : Type v}
[InvolutiveStar R]
[InvolutiveStar S]
:
InvolutiveStar (R × S)
@[implicit_reducible]
@[implicit_reducible]
instance
Prod.instStarAddMonoid
{R : Type u}
{S : Type v}
[AddMonoid R]
[AddMonoid S]
[StarAddMonoid R]
[StarAddMonoid S]
:
StarAddMonoid (R × S)
@[implicit_reducible]
instance
Prod.instStarRing
{R : Type u}
{S : Type v}
[NonUnitalNonAssocSemiring R]
[NonUnitalNonAssocSemiring S]
[StarRing R]
[StarRing S]
:
StarRing (R × S)
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)