Documentation

Mathlib.Algebra.Star.Prod

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.

source
instance Prod.instTrivialStar {R : Type u} {S : Type v} [Star R] [Star S] [TrivialStar R] [TrivialStar S] :
TrivialStar (R × S)
source
@[instance_reducible]
instance Prod.instInvolutiveStar {R : Type u} {S : Type v} [InvolutiveStar R] [InvolutiveStar S] :
InvolutiveStar (R × S)
source
@[instance_reducible]
instance Prod.instStarMul {R : Type u} {S : Type v} [Mul R] [Mul S] [StarMul R] [StarMul S] :
StarMul (R × S)
source
@[instance_reducible]
instance Prod.instStarAddMonoid {R : Type u} {S : Type v} [AddMonoid R] [AddMonoid S] [StarAddMonoid R] [StarAddMonoid S] :
StarAddMonoid (R × S)
source
@[instance_reducible]
instance Prod.instStarRing {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [StarRing R] [StarRing S] :
StarRing (R × S)
source
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)
source
theorem Units.embed_product_star {R : Type u} [Monoid R] [StarMul R] (u : Rˣ) :
(embedProduct R) (star u) = star ((embedProduct R) u)