# mathlib3documentation

algebra.star.prod

# star on product types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def prod.has_star {R : Type u} {S : Type v} [has_star R] [has_star S] :
has_star (R × S)
Equations
@[simp]
theorem prod.fst_star {R : Type u} {S : Type v} [has_star R] [has_star S] (x : R × S) :
@[simp]
theorem prod.snd_star {R : Type u} {S : Type v} [has_star R] [has_star S] (x : R × S) :
theorem prod.star_def {R : Type u} {S : Type v} [has_star R] [has_star S] (x : R × S) :
= ,
@[protected, instance]
def prod.has_trivial_star {R : Type u} {S : Type v} [has_star R] [has_star S]  :
@[protected, instance]
def prod.has_involutive_star {R : Type u} {S : Type v}  :
Equations
@[protected, instance]
def prod.star_semigroup {R : Type u} {S : Type v} [semigroup R] [semigroup S]  :
Equations
@[protected, instance]
def prod.star_add_monoid {R : Type u} {S : Type v} [add_monoid R] [add_monoid S]  :
Equations
@[protected, instance]
def prod.star_ring {R : Type u} {S : Type v} [star_ring R] [star_ring S] :
Equations
@[protected, instance]
def prod.star_module {R : Type u} {S : Type v} {α : Type w} [ R] [ S] [has_star α] [has_star R] [has_star S] [ R] [ S] :
(R × S)
@[simp]
theorem units.embed_product_star {R : Type u} [monoid R] (u : Rˣ) :
=